操作此（数组）字段时循环不变性不够强

Question

已更新

解决一些愚蠢问题的问题，下面用给定的 class 和相应的方法进行描述。如果您还需要其他东西，请告诉我，在此先感谢您。 link 也更新了 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

Answer 1

我发现很难理解您的代码应该做什么 - 主要是因为变量名称很难理解。所以我只是通过盲目加强不变量直到它通过来让它验证。在一种情况下，cut，我必须向该方法添加一个额外的前提条件。我不知道这是否适合您的情况，但我认为它确实反映了方法（目前的情况）的实际要求。

分配时需要给数组一个大小：

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

您需要将 "not null" 个事实添加到您的循环不变量中：

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

您需要添加足够的事实来确定数组访问是在边界内的，例如：

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

我强烈建议您使用切片而不是forall k量化。这样的 forall 量化很难正确，更难阅读，而且通常对验证者帮助不大：

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

this 对象在循环的修改集中。所以你需要说你的循环没有弄乱它的字段：

modifies this,scrap
invariant TextInv()

你需要说 scrap 数组中的对象仍然是方法的修改集中的对象：

invariant scrap == old(scrap)

其他说明：

如果您不需要变量具有负值，请考虑使用 nat 而不是 int
您通常可以通过从后置条件开始并向后工作来使其验证。只要不断加强不变量和前提条件，直到它起作用。当然，您可能会发现现在的先决条件太强了 - 如果是这样，您需要更强大的实现。

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

操作此（数组）字段时循环不变性不够强

Loop invariant not strong enough when manipulating (array) fields of this

formal-verification

compiler-errors

loop-invariant

dafny