Dafny“找不到触发条件”错误消息答案

【问题标题】：Dafny "no terms found to trigger on" error messageDafny“找不到触发条件”错误消息
【发布时间】：2016-07-24 02:26:09
【问题描述】：

我有一个数组line，其中包含一个长度为l 的字符串， pat 是另一个数组，其中包含一个长度为 p 的字符串。注意：p 和 l 不是数组的长度

目的是查看pat 中包含的字符串是否存在于line 中。如果是，则此方法应返回单词首字母在line 中的索引，否则应返回-1。

给我们“找不到触发条件”错误的不变量是ensures exists j :: ( 0<= j < l) && j == pos; 和invariant forall j :: 0 <= j < iline ==> j != pos;

我对循环的逻辑是，当它们在循环中时，找不到索引。并且保证是在遇到索引时。

可能出了什么问题？

代码如下：

method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int)
requires line!=null && pat!=null;
requires 0 <= l < line.Length; 
requires 0 <= p < pat.Length;
ensures exists j :: ( 0<= j < l) && j == pos;

{

var iline:int := 0;
var ipat:int  := 0;
var initialPos:int  := -1;

while(iline<l && ipat<pat.Length)
invariant 0<=iline<=l;
invariant 0<=ipat<=pat.Length;
invariant forall j :: 0 <= j < iline ==> j != pos;

{
    if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){
        if(initialPos==-1){
            initialPos := iline;
        }
        ipat:= ipat + 1;
    }
    else{
    if(ipat>0){
      if(line[iline] == pat[ipat-1]){
        initialPos := initialPos + 1;
      }
    }
        ipat:=0;
        initialPos := -1;
    }
    if(ipat==p){
        return initialPos; 
    }
    iline := iline + 1; 
}
return initialPos;
}

我收到以下错误： screenshot of Dafny output

这里是the code on rise4fun。

【问题讨论】：

标签： formal-verification dafny

【解决方案1】：

我认为你不需要使用量词来做出那些有问题的断言：

exists j :: ( 0<= j < l) && j == pos;

最好写成：

0 <= pos < l

和

forall j :: 0 <= j < iline ==> j != pos

同义：

pos >= iline

通过删除量词，您无需求解器实例化量词，因此不需要触发器。

另外，如果找不到模式，我认为您的方法将返回-1。因此，您需要考虑到这一点以使其验证：

method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int)
  requires line!=null && pat!=null
  requires 0 <= l < line.Length
  requires 0 <= p < pat.Length
  ensures 0 <= pos < l || pos == -1
{
  var iline:int := 0;
  var ipat:int  := 0;
  pos := -1;

  while(iline<l && ipat<pat.Length)
    invariant 0<=iline<=l
    invariant 0<=ipat<=pat.Length
    invariant -1 <= pos < iline
  {
      if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){
          if(pos==-1){
              pos := iline;
          }
          ipat:= ipat + 1;
      } else {
        if(ipat>0){
          if(line[iline] == pat[ipat-1]){
            pos := pos + 1;
          }
        }
        ipat:=0;
        pos := -1;
      }
      if(ipat==p) {
          return; 
      }
      iline := iline + 1; 
  }
  return;
}

http://rise4fun.com/Dafny/J4b0

【讨论】：