处理此数组的（数组）字段时，循环不变式不够强大 [英] Loop invariant not strong enough when manipulating (array) fields of this

问题描述

已更新

UPDATED

解决一些dafny问题的问题，下面将使用给定的类和相应的方法进行介绍。如果您需要其他东西，请告诉我，谢谢。链接也会使用rise4fun中的所有这些代码进行更新。

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

在rise4fun

推荐答案

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

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

您需要在循环不变式中添加 not null事实：

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

我强烈建议您使用切片而不是全部k 量化。很难正确地获得这样的 量化值，它很难阅读，并且对验证者的帮助通常较小：

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)

其他说明：

1. 使用 nat 代替 int 来代替，如果您不需要变量具有负值


2. 您通常可以通过从后置条件开始并向后工作来验证它。只是不断加强不变式和前提条件，直到它起作用。当然，您可能会发现现在的前提条件太强了-如果是这样，则需要更强大的实现。

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

这篇关于处理此数组的（数组）字段时，循环不变式不够强大的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！