WHAT IS A LOOP INVARIANT?

It is a predicate that holds at loop entry
and exit, no matter how many times we
execute the loop.

{x > y}
while x =! 0 loop
x := x - 2;
y := y - 2;
end loop;
{x > y and x = 0}

The invariant is {x > y}. The proof
rule can be used to show the above holds.

However, the loop may not terminate if
the variable x is odd upon entry of loop.