I'm using Dafny to make a delete method where you receive:
char array
line
the length of the array
l
a position
at
the number of characters to delete
p
First you delete the characters of line from at to at + p
, and then you must move all the characters on the right of at + p
to at
.
For example, if you have [e][s][p][e][r][m][a]
, and at = 3
, and p = 3
, then the final result should be [e][s][p][a]
I'm trying to prove a postcondition that makes sense like:
ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);
To ensure that all chars from the right of at + p are in the new positions.
But Dafny outputs two errors:
index out of range 7 53
postcondition might not hold on this return path. 19 2
method delete(line:array<char>, l:int, at:int, p:int)
requires line!=null;
requires 0 <= l <= line.Length && p >= 0 && at >= 0;
requires 0 <= at+p <= l;
modifies line;
ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]) ;
{
var tempAt:int := at;
var tempAt2:int := at;
var tempPos:int := at+p;
while(tempAt < at + p)
invariant at<=tempAt<=at + p;
{
line[tempAt] := ' ';
tempAt := tempAt + 1;
}
while(tempPos < line.Length && tempAt2 < at + p)
invariant at + p<=tempPos<=line.Length;
invariant at<=tempAt2<=at+p;
{
line[tempAt2] := line[tempPos];
tempAt2 := tempAt2 + 1;
line[tempPos] := ' ';
tempPos := tempPos + 1;
}
}