What makes a good loop invariant?

Let’s break down the question a bit…

What makes a valid loop invariant?

A loop invariant should hold

  1. Before the loop
  2. At the top of the loop body
  3. At the bottom of the loop body
  4. After the loop

It’s indeed the case that true is a valid loop invariant, but it’s rarely useful

What makes a useful loop invariant?

When annotating code with Hoare logic assertions, the invariant φ appears as follows:

{φ}
while (c)
    {φ ∧ c}
    ...loop body...
    {φ}
{φ ∧ ¬c}

These code annotations give rise to so called proof obligations: If two assertions end up next to each other

...
{α}
{β}
...

then you’re obliged to show that α → β. So, in the example above, you’ll presumably know what’s true before the loop and what needs to be true after the loop. For the loop invariant φ to be useful you thus need to make sure the following implications hold:

The second implication disqualifies true as a useful loop invariant, as true → something only holds if something holds by itself. (Put differently, if we choose true as our loop invariant, we have no “help” from it when reasoning about the code below the loop.)

Finally: What makes a good loop invariant?

Apart from being valid and useful, it’s nice if it’s

Comments

Be the first to comment!