Axiomatic Semantics: Loop Invariants

Overview

To refresh your memory about loop invariants, remember that we are working with a bit of code such as this:

    {PRECONDITION}
    while (CONDITION) do
        BODY
    end
    {POSTCONDITION}

1. P ==> I: The PRECONDITION before the loop implies the INVARIANT.

2. {I} B {I}: If the INVARIANT is true before CONDITION is evaluated, it is also true after.

3. {I and B} BODY {I}: If the INVARIANT and the CONDITION are both true before the BODY, then the INVARIANT will be true after the BODY

4. (I and not B) ==> Q: If the INVARIANT is true and the CONDITION is false, that implies that the POSTCONDITION must be true

Example 1

The first example:

    { true }                      (* precondition *)
    i := 10;
    total := 0;
				  (* just before loop *)
    while (i > 0) do
        total := total + i;
	i := i - 1;
    end
    { total = sum from 1 to 10 }  (* postcondition *)

What loop invariant should we use for this code segment?

To start, note that just before the loop above we know that { i = 10 and total = 0 }.

To determine the loop invariant, start by looking at what is going on inside the loop. This particular loop is counting down from 10 to 0, and at each step i is being added to total.

    time                     i    total
    ---------------         --   -----
    before loop             10       0
    after 1st iteration      9      10
    after 2nd iteration      8      10 + 9
    ...
    after last iteration     0      10 + 9 + ... + 1

From this, we can generalize a trend. Each time through the loop, total is equal to the sum from i+1 to 10. We can take this as our first try at an invariant:

    INVARIANT = { total = sum from i+1 to 10 }

Finally, look at condition 4: is it true that (I and not B) implies Q? That is, does ((total = sum from i+1 to 10) and i <= 0) imply that (total = sum from 1 to 10)? Unfortunately no, since it does not restrict the value of i to 0. That means we need a stronger loop invariant.

In this case, we can strengthen the loop invariant by including the fact that i >= 0, giving:

    INVARIANT = { total = sum from i+1 to 10 and i >= 0 }

Example 2

For another example, consider working with a stack object called "stack":

    len := 0;
    while (not stack.is_empty ()) do
        len := len + 1;
	stack.pop ();
    end
    { len = length of the stack before the loop }  (* postcondition *)

What loop invariant should we use for this code segment?

To start, note that just before the loop above we know that { len = 0 }.

To determine the loop invariant, start by looking at what is going on inside the loop. This particular loop is measuring the length of the stack. Let's call the stack contents before the loop starts the "old stack", and the contents at the current point of execution the "new stack". Then we can talk about the length of the stack before the loop as "|old stack|".

    time                    len    # elements in stack
    ---------------         ---    -------------------
    before loop              0        |old stack|
    after 1st iteration      1        |old stack| - 1
    after 2nd iteration      2        |old stack| - 2
    ...
    after last iteration  |old stack|     0

From this, we can generalize a trend. Each time through the loop, len plus the number of elements now in the stack is equal to the length of the original stack. We can take this as our first try at an invariant:

    INVARIANT = { |old stack| = len + |new stack| }

Finally, look at condition 4: is it true that (I and not B) implies Q? That is, does (|old stack| = len + |new stack|) and the new stack is empty) imply that (len = |old stack|)? Fortunately, this time it does. Since the new stack is empty, |new stack| = 0. That means:

     |old stack| = len + |new stack|
     |old stack| = len + 0
     |old stack| = len

In this case, we arrived at our loop invariant on the first guess.

Discussion

Notice how the two examples above are solved. Loop invariants can include up to three separate bits of information.

1. They include information about the work being done by the loop. You can think of this as the "incrementally computed" state produced by the loop--it captures all the work done by the iterations completed so far, but not any of the future iterations that have not yet occurred.

2. The loop invariant may also need to carry information about the "index variable", that is the main variable (or variables) that control when the loop terminates. If the termination condition for the loop is not specific enough to pin down the index variable to a single value, this extra information in the loop invariant may be necessary, as in Example 1 above (i >= 0). At other times, the loop's termination condition may be strong enough that this extra information is not required in the invariant (as in Example 2).

3. Since P ==> I, and (I and not B) ==> Q, there is no direct connection between the precondition and the postcondition for the loop. That means that if P contains any information about variables that are not involved in the loop at all, the only way that same information can be present in the postcondition is if it is "passed through" by the invariant. Neither of the examples above show this directly.

   For an example, consider modifying the code for Example 2 above as follows:

       x := 17;
       len := 0;
       while (not stack.is_empty ()) do
           len := len + 1;
   	stack.pop ();
       end
       { len = length of the stack before the loop and x = 17 }
   

   Now, in order to establish the postcondition, we would need to add "x = 17" to the original invariant that we developed. This clause states what the loop doesn't change. Sometimes that is just as important as stating what the loop does modify.