函数中的 Dafny 语法错误

Question

我正在为愚蠢的语法苦苦挣扎。

searchAndReplace 接收三个字符数组。假设 line 是 [s][n][a][k][e]； pat 是 [n][a] 并且 dst 是 [h][i]。我想在 line 中搜索所有出现的 pat 并将其替换为 dst 导致 [s][h][i][k][e]

方法find将returnline中第一个字母的索引等于pat。

方法 delete 将从变量 at return 处的 line 中删除 pat，并移动所有其他变量at+p 之后的元素向左移动以填充空 spaces.

方法insert将使space通过移动[=28=之间的所有字符来将dst添加到lineat at ]和at + pp右边的位置。

我创建了一个辅助函数，它将比较 pat 和 dst 以验证它们不相等（如果它们相等，它将无限次替换 dstin line 以防 pat 存在于 line 中）现在我在函数 checkIfEqual 内的以下代码部分收到错误“then expected”：

if(pat.Length != dst.Length) {
    return false;
   }

完整代码：

    method searchAndReplace(line:array<char>, l:int,
        pat:array<char>, p:int,
        dst:array<char>, n:int)returns(nl:int)
        requires line != null && pat!=null && dst!=null;
        requires !checkIfEqual(pat, dst);
        requires 0<=l<line.Length;
        requires 0<=p<pat.Length;
        requires 0<=n<dst.Length;

        modifies line;
        {
          var at:int := 0;
          var p:int := n;

          while(at != -1 )
          invariant -1<=at<=l;
          {
            at := find(line, l, dst, n);
            delete(line, l, at, p);
            insert(line, l, pat, p, at);
          }

          var length:int := line.Length;

          return length;
        }

        function checkIfEqual(pat:array<char>, dst:array<char>):bool
        requires pat!=null && dst!=null;
        reads pat;
        reads dst;
         {

          var i:int := 0;

          if(pat.Length != dst.Length) {
           return false;
           }

          while(i<dst.Length) {
            if(pat[i] != dst[i]){
              return false;
            }
            i := i + 1;
          }
          return true;

        }

        method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int)
          requires line != null && nl != null;
          requires 0 <= l+p <= line.Length && 0 <= p <= nl.Length ;
          requires 0 <= at <= l;
          modifies line;
          ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error
        {
          var i:int := 0;
          var positionAt:int := at;
          while(i<l && positionAt < l)
            invariant 0<=i<l+1;
            invariant at<=positionAt<=l;
          {
            line[positionAt+p] := line[positionAt];
            line[positionAt] := ' ';
            positionAt := positionAt + 1;
            i := i + 1;
          }

          positionAt := at;
          i := 0;
          while(i<p && positionAt < l)
            invariant 0<=i<=p;
            invariant at<=positionAt<=l;
          {
            line[positionAt] := nl[i];
            positionAt := positionAt + 1;
            i := i + 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;
        }
  method delete(line:array<char>, l:nat, at:nat, p:nat)
  requires line!=null
  requires l <= line.Length
  requires at+p <= l
  modifies line
  ensures line[..at] == old(line[..at])
  ensures line[at..l-p] == old(line[at+p..l])
{
  var i:nat := 0;
  while(i < l-(at+p))
    invariant i <= l-(at+p)
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at])
    invariant line[at..at+i] == old(line[at+p..at+p+i])
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched
  { 
    line[at+i] := line[at+p+i];
    i := i+1;
  }
}

Answer 1

Dafny 中的

function 是纯粹的、归纳定义的，并且使用与命令式 methods 不同的语法。您不能在函数内使用命令式语言功能。在这种情况下，您不允许使用：

条件语句if cond { s1* } else { s2* }
循环语句while cond { s1* }

函数体必须是表达式：

predicate checkIfEqual(pat:array<char>, dst:array<char>)
  requires pat!=null && dst!=null;
  reads pat;
  reads dst;
{
     pat.Length == dst.Length 
  && forall i:nat :: i < pat.Length ==> pat[i] == dst[i]
}

虽然这里不需要，但是Dafny确实有一个条件表达式（ite）：

predicate checkIfEqual(pat:array<char>, dst:array<char>)
  requires pat!=null && dst!=null;
  reads pat;
  reads dst;
{
  if pat.Length != dst.Length then false 
  else forall i:nat :: i < pat.Length ==> pat[i] == dst[i]
}

注意：

不能在函数体中放入循环，但可以使用递归
predicate 是 shorthand 对于 function 那 returns bool

函数中的 Dafny 语法错误

Dafny syntax error in function

dafny