HAVOC in Dafny

Apr 29, 2013 at 5:03 AM
Just wondering whether Dafny has a statement
havoc x,y,z;
At the moment I'm using
x,y,z:| true;
But havoc would be neater.
Apr 29, 2013 at 7:53 AM
Yes, you can write a * as the right-hand side of an assignment. For example, like this:
x, y, z := *, *, *;
Or mix it with other assignments, if you have a need to:
a, b, c := a+1, *, c/2 + b%2
Rustan