Move invariants to end of do-while loop?

Sep 7, 2011 at 11:41 AM

Some code using a while-do loop:

int x = 5;
int y = 8;
while(x>0) 
_(invariant x>=0 && y==8)
{
  x--;
  y=8;
}
_(assert x==0 && y==8)

Now I convert it to a do-while loop, and omit the initialisation of y, knowing that the loop will do that for me:

int x = 5;
int y;
do
_(invariant x>0)
{
  x--;
  y=8;
}
while(x>0);
_(assert x==0 && y==8)

It is now a little tricky to write the loop invariant. I can no longer say y==8, because that doesn't hold on the first iteration. And the x>=0 has become x>0, which is slightly surprising. I would argue that the loop invariant for a do-while loop should be written at, and required to hold at, the *end* of the loop body. Then my code becomes:

int x = 5;
int y;
do
{
  x--;
  y=8;
}
_(invariant x>=0 && y==8)
while(x>0);
_(assert x==0 && y==8)

which is much closer to the original while-do version, and, for me at least, feels quite a bit more intuitive. What do people think?

Developer
Sep 25, 2011 at 5:36 PM
Edited Sep 25, 2011 at 5:39 PM

There are two problems with putting the invariant at the bottom of the loop:

- It introduces a disjunction at the top of the loop: you know that either this is the first time through the loop or the invariant holds. Now, when some assertion fails in the middle of the loop body, there is confusion about whether it was on the first iteration (i.e., the code prior to the loop wasn't strong enough) or a subsequent iteration (i.e., the loop invariant wasn't strong enough). Conversely, with the invariant at the top, you can distinguish between these cases.

- A basic principle of sequential program verification is that you should be able to read a function from top to bottom and judge its correctness. Without knowing the loop invariant, we can't tell whether there is a bug in the loop body when we read it.

A possible alternative is to introduce a built-in predicate like \loop_entry that represents the strongest postcondition of the code preceding the loop. Then instead of writing _(invariant  p) at the bottom of the loop, you could write _(invariant \loop_entry() || p) at the top of the loop.