Dafny "Call may violate context's modifies clause"

user_8895427 0
Viewed 1113

I'm attempting to verify a hashset but I've run into a problem with my insert method.

I don't understand why I'm getting the "call may violate context's modifies clause" error when I uncomment the inserts in main. I believe it to be something to do with the use of fresh, but I'm unclear on how / where to do this.

Code can be found at : https://rise4fun.com/Dafny/9UDG

dafny
1 Answers

The problem is that insert claims to modify this and a, which leaves open the possibility that the first call to insert changes the a field to point to something arbitrary, and then the second call to insert modifies that arbitrary thing.

A simple solution is to add ensures a == old(a) to insert.

user_4382670
Related