invariant over while instead of under it

Nov 28, 2013 at 4:15 PM
I would like to comment that, in my opinion, the invariant should be written in the line just over the word while instead of in the line under it. Actually,, the control point which states the invariant represents is before the boolean condition of the while is evaluated. Could someone tell me why in Dafny the invariant should be written after that condition?
Dec 3, 2013 at 9:20 PM
Thanks. Yes, I understand completely. Eiffel does it this way, for example. The (historical) reason for this is that it makes loops aesthetically similar to methods. Compare:
method MyMethod(x: int)
  requires x <= 100;
  // method body
while y < 100
  invariant y <= 100;
  // loop body
I don't know if this will change, but I am aware of the issue and appreciate the feedback.

Dec 4, 2013 at 8:42 AM

Hi Rustan,

Thank you for your quick answer.

After I had written the post, I realized that Dafny distinguishes between the invariant location and

the assertion location just after the “left curly brace” that starts the while-body.

The former corresponds to where the conjunction of, both, the invariant and the while-condition, is satisfied.

I think that such distinction is important to justify the Dafny location for invariants.

Although I was costumed to write the invariant before the while, now I like the Dafny-style.