empty while loops

Feb 24, 2016 at 11:40 PM
Dafny allows empty while loops (and from looking at the grammar, not just by accident). The compiler refuses to generate code for them; more alarmingly, the generated Boogie code seems to be "assume false." Do such loops have an intended purpose?

(I discovered this by accident when a student accidentally used the keyword "assert" instead of "invariant" after the "while (...)" and assumed all was well, because the method post-conditions were all proved!)
Coordinator
Feb 25, 2016 at 6:41 PM
Yes, Dafny allows body-less loops. (I'm intrigued that you're looking into the generated Boogie code to get more details. :)) The body-less loops are an experimental feature that hasn't fully been implemented yet. To avoid the sort of confusion that you report the student experienced (and which I've heard once before as well), it would be good to give feedback in the Visual Studio and emacs IDEs that the loop is missing a body. (It would be good to file this as an Issue to make sure we do address it.)

Let me explain the motivation behind the body-less loops.

If you're writing the body of a method A, you may choose to relegate some of its behavior to another method, B. At that time in the development process, you define method B, writing its signature and specification. Then, you're faced with a choice: you may want to concentrate on supplying an implementation (body) of B or you may prefer to postpone that task until you have finished writing the rest of A.

Something similar happens when you in method A discover the need for a loop. At that time, you define the loop by writing down its guard and invariant. Once you've done that, you would like to have the same choice as when you break out some of the computation into the separate method B: either concentrate on supplying an implementation (body) for the loop or first finish writing the code that follows the loop. Body-less loops in Dafny give you this choice. In other words, the fact that you're not supplying a body for the loop should be considered a temporary situation in your program development--you will return to supply the loop body later, once you've expressed and verified the code that will follow the loop.

It is possible do something quite similar even if loop bodies were syntactically required (and, analogously, if method bodies were always syntactically required), namely to give the body as { }. However, if you write an empty body, Dafny sees that nothing is modified, which results in a loop translation where in effect you're not getting the full verification of the program downstream of the loop. The intent behind the body-less loop was to do better. The tricky thing is to guess what the loop was intending to modify. Guessing heap modifications is easy--use as the guess the modifies clause of the enclosing method (for the analogous body-less method case, the caller uses the modifies clause and that's everything that's needed). Guessing which local variables are to be modified by the loop requires some heuristics. We intended to develop such heuristics as part of this body-less-loop effort, but I'm afraid this effort has been stalled for some time, given other priorities.

There's another possible advantage with having body-less loops (as opposed to writing a loop with an empty body). It is that the body-less loop invites a clever compiler to do some synthesis (you are welcome to read this: it invites a professor with a clever student to do some synthesis). It would be wonderful, as a developer, to be able to write a loop guard+invariant but without a body, continue writing the program after the loop, and then get a little indication from the IDE that says "hey, about this loop, don't bother filling in its body, I synthesized some code for it!".

Rustan
Marked as answer by rustanleino on 2/25/2016 at 11:41 AM
Developer
Feb 26, 2016 at 12:40 AM
From the command line, you can use /noCheating:1, which will cause Dafny to complain about methods and functions that are missing a body (unless you give them the :axiom annotation). If it doesn't already, it should also object to body-less while loops. If it doesn't that would be worth filing a bug as well.