Some code using a whiledo 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 dowhile 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 dowhile 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 whiledo version, and, for me at least, feels quite a bit more intuitive. What do people think?
