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 14, 2014 at 11:10 PM by howell, version 1


No comments yet.