Dafny context modifies clause error

Question

i am having a really hard time getting rid of the last error in my Dafny program. Can someone point me in the right direction? Here is the code: http://rise4fun.com/Dafny/2FPo

I am getting this error: assignment may update an array element not in the enclosing context's modifies clause

I tried adding modifies rectangle in the merge method (even though i am pretty sure that is already included in modifies this) but that just creates a similar error on the merge method call.

I am really lost on this one. Thanks for the help

Answer 1

The problem is that "modifies this" allows modification of the fields of this, not modification of the things pointed to by those fields. In other words, it would be appropriate if the method was doing:

this.rectangles := new_rectangle_array;

but not if it was doing:

this.rectangles[3] := new_rect;

So, in the places you have "modifies this" you should instead have "modifies rectangles".

For a similar reason, Test needs to be annotated with "modifies c.rectangles", not "modifies c".

Finally, to convince Dafny that it's OK to call Test, you need to give the constructor for Couverture a post-condition constraining the rectangles field. Otherwise, the verifier can't be sure that it's OK to call Test: as far as the verifier can tell, couv might contain some random array that Main isn't allowed to modify.

For the full code, see http://rise4fun.com/Dafny/Skrg.