If you have a loop whose invariant takes in more and more of a sequence with each iteration, DafnyCC will typically need you to explicitly assert the relationship between the old sequence and the new sequence. For instance:
while j < |a|
    invariant a[..j] == b[..j];
{
    a[j] := b[j];
    assert a[..j+1] == a[..j] + [a[j]];   // this line added for DafnyCC's sake
    assert b[..j+1] == b[..j] + [b[j]];  // this line added for DafnyCC's sake
    j := j + 1;
}

This also applies to sequences derived from arrays. For instance, in the example above, the reminders above are necessary whether a and b are sequences or arrays.


Last edited Oct 15, 2014 at 12:10 AM by howell, version 1

Comments

No comments yet.