Loop invariant not strong enough when manipulating

问题:

UPDATED

Problems on solving some dafny problems, described below with the given class and respective methods. If you need something else please tell me, thank you in advance. Also the link is updated with all this code in rise4fun.

class TextEdit {
var text:array<char>; //conteúdo
var scrap: array<char>; //conteúdo temporariamente guardado para copy/paste
var tlen:int; //length di text
var slen:int; //length di scrap
var at:int; //current position
var sellen:int; //length of the selection


method key(ch:char)
modifies this, text;
requires TextInv();
requires tlen+1<text.Length && sellen == 0;
ensures TextInv();
{
  var tempChar:array<char> := new array<char>;
  tempChar[0] := ch;

  insert(text, tlen, tempChar, 1, at );   
  at := at + 1;
  tlen := tlen + 1;
}


method select(sel:int, sl:int)
modifies this;
requires TextInv() && 0 <= sel && 0 <= sl && 0 <= sel+sl <= tlen;
ensures TextInv();
{
  at := sel; 
  sellen := sl;
}

method copy()
modifies this,scrap;
requires TextInv() && sellen > 0;
requires scrap != null;
ensures TextInv();
ensures slen == sellen;
{

  //emptying scrap
  delete(scrap, slen, 0, slen);
  slen := 0;

  var i:int := 0;
  while(i<sellen)
  invariant 0<=i<=sellen;
  invariant slen == i;
  //cada posição do scrap estará vazia 
  //invariant forall j :: 0<=j<i ==> scrap[j] == ' ';
  //só depois será preenchida
  invariant forall k :: i<=k<sellen ==> scrap[k] == text[at+k];
  {
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1;
  }

}

method cut()
requires scrap!=null && text!=null;
modifies this,text, scrap;
requires TextInv() && sellen > 0;
ensures TextInv();
ensures slen == sellen;
{
  //emptying scrap
  delete(scrap, slen, 0, slen);
  slen := 0;

  var i:int := 0;
  while(i<sellen)
  invariant i<=0<=sellen;
  //cada posição do scrap estará vazia 
 // invariant forall j :: 0<=j<i ==> scrap[j] == ' ';
  //só depois será preenchida
  invariant forall k :: i<=k<sellen ==> scrap[k] == text[at+k];
  {
    scrap[i] := text[at+i]; 
    slen := slen + 1;  
    i := i + 1;
  }
  delete(text, tlen, at, sellen);

  tlen := tlen - slen;
  }


method paste()
modifies this,text;
requires TextInv() && 0 <= slen+tlen < text.Length && sellen == 0;
ensures TextInv();
ensures tlen == old(tlen)+slen;
ensures at == old(at)+slen;
{
  if(slen>0)
  { 
    insert(text, tlen, scrap, slen, at );
    tlen := tlen + slen;
    at := at + slen;
  } 
}

function TextInv():bool 
reads this;
{
 text != null && 0 <= tlen <= text.Length && scrap != text &&
 0 <= at <= tlen && 0 <= sellen && 0 <= at+sellen <= tlen &&
 scrap != null && 0 <= slen <= scrap.Length == text.Length
}
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 // line has enough space
  requires 0 <= p <= nl.Length // string in nl is shorter than nl
  requires 0 <= at <= l // insert position within line
  modifies line
  ensures line != null;
  ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now
{
  ghost var initialLine := line[..];

  // first we need to move the characters to the right
  var i:int := l;
  while(i>at)
    invariant line[0..i] == initialLine[0..i]
    invariant line[i+p..l+p] == initialLine[i..l]
    invariant at<=i<=l
  {
    i := i - 1;
    line[i+p] := line[i];
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at+p..l+p] == initialLine[at..l];

  i := 0;
  while(i<p)
    invariant 0<=i<=p
    invariant line[0..at] == initialLine[0..at]
    invariant line[at..at+i] == nl[0..i]
    invariant line[at+p..l+p] == initialLine[at..l]
  {
    line[at + i] := nl[i];
    i := i + 1;
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at..at+p] == nl[0..p];
  assert line[at+p..l+p] == initialLine[at..l];
}

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!=null
  ensures line[..at] == old(line[..at])
  ensures line[at..l-p] == old(line[at+p..l])
  ensures forall i :: l-p <= i < l ==> line[i] == ' '  
{
  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;
  }

  var j:nat := l-p;
  while(j < l)
    invariant l-p <= j <= l
    invariant line[..at] == old(line[..at])
    invariant line[at..l-p] == old(line[at+p..l])
    invariant forall i :: l-p <= i < j ==> line[i] == ' '
  {
    line[j] := ' ';
    j := j+1;
  }
}
}

On rise4fun

回答1:

I found it hard to understand what your code is supposed to do - mostly because the variables names are difficult to understand. So I have just made it verify by blindly strengthening the invariants until it passed. In one case, cut, I had to add an additional precondition to the method. I do not know if this is appropriate to your situation or not, but I think it does reflect what the method (as it stands) actually requires.

You need to give the array a size when you allocate it:

var tempChar:array<char> := new char[1];

You need to add "not null" facts into your loop invariants:

invariant scrap != null && text != null;

You need to add sufficient facts to establish that the array accesses are in bounds, e.g:

invariant sellen <= scrap.Length
invariant at+sellen <= text.Length
invariant 0 <= at

I strongly recommend that you use slices rather than the forall k quantification. It is difficult to get such forall quantification correct, it is harder to read, and is often less helpful for the verifier:

invariant scrap[..i] == text[at..at+i];

The this object is in the modifies set of your loop. So you need to say that your loop didn't mess up its fields:

modifies this,scrap
invariant TextInv()

You need to say that the object in the scrap array is still the same one that is in the modifies set of the method:

invariant scrap == old(scrap)

Other notes:

1. considier using nat instead of int if you don't need a variable to have negative values
2. you can often make it verify by starting from the postcondition and working backwards. Just keep strengthening the invariants and preconditions till it works. Of course, you may find out the preconditions are now too strong - if so you need a more capable implementation.

http://rise4fun.com/Dafny/GouxO

class TextEdit {
var text:array<char>; //conteúdo
var scrap: array<char>; //conteúdo temporariamente guardado para copy/paste
var tlen:int; //length di text
var slen:int; //length di scrap
var at:int; //current position
var sellen:int; //length of the selection


method key(ch:char)
modifies this, text;
requires TextInv();
requires tlen+1<text.Length && sellen == 0;
ensures TextInv();
{
  var tempChar:array<char> := new char[1];
  tempChar[0] := ch;

  insert(text, tlen, tempChar, 1, at );   
  at := at + 1;
  tlen := tlen + 1;
}


method select(sel:int, sl:int)
modifies this;
requires TextInv() && 0 <= sel && 0 <= sl && 0 <= sel+sl <= tlen;
ensures TextInv();
{
  at := sel; 
  sellen := sl;
}

method copy()
modifies this,scrap;
requires TextInv() && sellen > 0;
requires scrap != null;
ensures TextInv();
ensures slen == sellen;
{
  //emptying scrap
  delete(scrap, slen, 0, slen);
  slen := 0;

  var i:nat := 0;
  while(i<sellen)
    modifies this,scrap
    invariant TextInv()
    invariant 0<=i<=sellen;
    invariant slen == i;
  //cada posição do scrap estará vazia 
  //invariant forall j :: 0<=j<i ==> scrap[j] == ' ';
  //só depois será preenchida
    invariant scrap != null && text != null;
    invariant sellen <= scrap.Length
    invariant at+sellen <= text.Length
    invariant 0 <= at
    invariant scrap[0..i] == text[at..at+i];
    invariant scrap == old(scrap)
  {
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1;
  }
}

method cut()
//requires scrap!=null && text!=null;
modifies this,text, scrap;
requires TextInv() && sellen > 0;
requires 0 <= at+sellen <= (tlen - (slen + sellen));
ensures TextInv();
ensures slen == sellen;
{
  //emptying scrap
  delete(scrap, slen, 0, slen);
  slen := 0;

  assert 0 <= at+sellen <= (tlen - (slen + sellen));

  var i:int := 0;
  while(i<sellen)
  invariant 0<=i<=sellen;
  //cada posição do scrap estará vazia 
  //invariant forall j :: 0<=j<i ==> scrap[j] == ' ';
  //só depois será preenchida
  invariant scrap != null && text != null;
  invariant i <= scrap.Length
  invariant 0 <= at
  invariant at+i <= text.Length
  invariant scrap[0..i] == text[at..at+i];
  invariant slen + (sellen-i) <= scrap.Length;
  invariant slen + (sellen-i) == sellen;
  invariant TextInv()
  invariant scrap == old(scrap)
  invariant text == old(text)
  invariant 0 <= at+sellen <= (tlen - (slen + (sellen-i)));
  {
    scrap[i] := text[at+i]; 
    slen := slen + 1;  
    i := i + 1;

    /*assert text != null; 
    assert 0 <= tlen <= text.Length ; 
    assert scrap != text ; 
    assert 0 <= at <= tlen ; 
    assert 0 <= sellen ; 
    assert 0 <= at+sellen <= tlen ; 
    assert scrap != null ; 
    assert 0 <= slen <= scrap.Length == text.Length;*/
  }

  assert 0 <= at+sellen <= (tlen - slen);

  delete(text, tlen, at, sellen);

  assert 0 <= at+sellen <= (tlen - slen);

  tlen := tlen - slen;

  assert 0 <= at+sellen <= tlen ; 
}


method paste()
modifies this,text;
requires TextInv() && 0 <= slen+tlen < text.Length && sellen == 0;
ensures TextInv();
ensures tlen == old(tlen)+slen;
ensures at == old(at)+slen;
{
  if(slen>0)
  { 
    insert(text, tlen, scrap, slen, at );
    tlen := tlen + slen;
    at := at + slen;
  } 
}

function TextInv():bool 
reads this;
{
 text != null && 0 <= tlen <= text.Length && scrap != text &&
 0 <= at <= tlen && 0 <= sellen && 0 <= at+sellen <= tlen &&
 scrap != null && 0 <= slen <= scrap.Length == text.Length
}
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 // line has enough space
  requires 0 <= p <= nl.Length // string in nl is shorter than nl
  requires 0 <= at <= l // insert position within line
  modifies line
  ensures line != null;
  ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now
{
  ghost var initialLine := line[..];

  // first we need to move the characters to the right
  var i:int := l;
  while(i>at)
    invariant line[0..i] == initialLine[0..i]
    invariant line[i+p..l+p] == initialLine[i..l]
    invariant at<=i<=l
  {
    i := i - 1;
    line[i+p] := line[i];
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at+p..l+p] == initialLine[at..l];

  i := 0;
  while(i<p)
    invariant 0<=i<=p
    invariant line[0..at] == initialLine[0..at]
    invariant line[at..at+i] == nl[0..i]
    invariant line[at+p..l+p] == initialLine[at..l]
  {
    line[at + i] := nl[i];
    i := i + 1;
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at..at+p] == nl[0..p];
  assert line[at+p..l+p] == initialLine[at..l];
}

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!=null
  ensures line[..at] == old(line[..at])
  ensures line[at..l-p] == old(line[at+p..l])
  ensures forall i :: l-p <= i < l ==> line[i] == ' '  
{
  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;
  }

  var j:nat := l-p;
  while(j < l)
    invariant l-p <= j <= l
    invariant line[..at] == old(line[..at])
    invariant line[at..l-p] == old(line[at+p..l])
    invariant forall i :: l-p <= i < j ==> line[i] == ' '
  {
    line[j] := ' ';
    j := j+1;
  }
}
}