Emit a warning when "old" does nothing in a specification
val swap (t : array int) (i j : int): unit
requires { 0 <= i < length t /\ 0 <= j < length t }
ensures { t = (old t)[i <- old t[j]][j <- old t[i]] }
In the example above, I wrote a specification for the swap function but forgot the writes
clause. My impression is that an old
in a specification where nothing under the old
is in the writes is almost always a user error, and that we should emit a "Maybe you forgot a writes
clause" warning.