
For the following program, Dafny reported: "Error: This loop invariant might not hold on entry."
method LoopInvProblem(n: int) returns (result: int)
requires 1 <= n;
ensures result == n;
{
var i := 0;
while (i < n)
invariant i <= n;
{
i := i + 1;
}
if (n <= 0) { // loop skipped
result := n;
} else {
result := i;
}
}
When the requires clause is changed to "requires 0 <= n;" the program verifies with no errors. Note that the offending invariant is weaker than the loop condition; values of n that are less than or equal to zero cause the loop to be skipped. I
discovered this while looking at variations to the binary search given in the Dafny tutorial. (In binary search, I set high := a.Length  1 and made appropriate changes in the code, but doing so caused the same type of problem with the loop invariant.)
Is this a known issue?
Thanks,
Greg K



This is the correct behavior. Loop invariants (e.g., see
Wikipedia) have to hold before the loop as well as at the end of every iteration. The loop guard is irrelevant to check whether the invariant holds at the beginning.



Thanks Stefan,
The way I was taught was that the loop invariant must hold at the beginning and end of each iteration of the loop body, so the guard can be assumed for everything but the end of the last iteration (where the guard necessarily fails).
I went back to Hoare's "Axiomatic Basis for Computer Programming" paper (see
CiteSeerX) and found this: "A slightly more powerful formulation is possible in light of the fact that B [the guard] may be assumed to be true on initiation of S:" and
then goes on to state his Rule of Iteration.
What I take from this is that Hoare's rule considers the guard, but it is not necessary to do so. Obviously Dafny does not.
Perhaps it is because I learned invariants the other way, but I'm having trouble coming up with an invariant that works for this obviously correct method. Can you (or someone else) tell me an invariant that makes this method verify in Dafny?
Thanks,
Greg
PS. I claim that the program is obviously correct because is verifies in Dafny when we have "requires 0 <= n", and it works correctly for n = 1 (because it skips the loop and sets "result := n").
+++++++++++++++++++
method LoopInvProblem(n: int) returns (result: int)
requires 1 <= n;
ensures result == n;
{
var i := 0;
while (i < n)
invariant i <= n;
{
i := i + 1;
}
if (n <= 0) { // loop skipped
result := n;
} else {
result := i;
}
}


Dec 18, 2012 at 4:19 PM
Edited Dec 18, 2012 at 4:19 PM

Sure, here is a version of your program that verifies:
method LoopInvProblem(n: int) returns (result: int)
requires 1 <= n;
ensures result == n;
{
var i := 0;
while (i < n)
invariant i <= n  n == 1;
{
i := i + 1;
}
if (n <= 0) { // loop skipped
result := n;
} else {
result := i;
}
}



Also, Dafny does implement the correct checks, and it corresponds to what you found in your citation. The rule there is
If "{ P and B } S { P }", then "{ P } while B do S { not B and P }"
In the conclusion you have the loop invariant P as the precondition of the statement. That is, if one can show "{ P and B } S { P }", then one can conclude that, given P holds before the loop, then "not B and P" holds after the
loop. But P has to hold at the beginning of the loop, regardless of whether B holds or not. At least if you define the rule like this, which is also what Dafny implements.



Thanks for the quick responses Stefan!
Greg

