Инвариант цикла недостаточно силен при манипулировании (массивом) полями этого

Мне было трудно понять, что должен делать ваш код, в основном потому, что имена переменных трудно понять. Так что я только что заставил его проверить, слепо усилив инварианты, пока он не прошел. В одном случае, cut, мне пришлось добавить в метод дополнительное предварительное условие. Я не знаю, подходит ли это к вашей ситуации или нет, но я думаю, что это действительно отражает то, что на самом деле требует метод (в его нынешнем виде).

Вам нужно указать размер массива при его выделении:

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

Вам нужно добавить «не нулевые» факты в ваши инварианты цикла:

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)

Другие примечания:

1. рекомендуется использовать nat вместо int, если вам не нужна переменная с отрицательными значениями
2. вы часто можете заставить его проверить, начав с постусловия и работая в обратном направлении. Просто продолжайте усиливать инварианты и предварительные условия, пока это не сработает. Конечно, вы можете обнаружить, что предварительные условия слишком сильны — если это так, вам нужна более мощная реализация.

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