1

I am struggling with dafny syntax.

searchAndReplace receives three arrays of chars. Let's imagine line is [s][n][a][k][e]; pat is [n][a] and dst is [h][i]. I want to search for all the occurrences of pat in line and replace it with dst resulting in [s][h][i][k][e]

Method findwill return the indice of the first letter in line that is equal to pat.

Method deletewill remove pat from line at the variable at returned at find, and move all the others elements after at+p to the left in order to fill the null spaces.

Method insertwill make space in order to dst be added to lineat atby moving all the characters between atand at + p ppositions to the right.

I created an auxiliar function which will compare patand dst in order to verify that they aren't equal(if they were it would be replacing infinitely time dstin line in case patexisted in line) For now i'm receiving the error "then expected" on the following section of code inside function checkIfEqual: 

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

The full code:

    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;
  }
}
4

1 回答 1

2

functionDafny 中的 s 是纯粹的、归纳定义的，并且使用与命令式不同的语法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]
}

注意：

  • 不能在函数体中放置循环，但可以使用递归

  • predicatefunction是返回的 a 的简写bool

于 2016-04-22T13:35:21.100 回答