Loop invariant: decreasing a variable and swapping it

Question

As an example exercise, we were asked to find the loop invariant for this bit of code.

def mystery(a,b):
    # Precondition: a >= 0 and b >= 0
    while a >= 0 and b >= 0:
        if a < b:
            a, b = b, a
        else:
            a = a - 1
    return a

From what I can see, it first ensures that a >= b.
After that, each loop iteration decreases the value of a by 1.

This will continue until a and b are 0.

Then one final iteration terminates the loop with a == -1.

However from what I can tell, if the loop invariant is something like a >= b, it fails upon termination as a = -1 and b = 0.

Could anyone tell me the actual loop invariant of this function as I'm a bit confused.

Answer 1

There isn't a single loop invariant: any property that remains true during the execution of the loop is a loop invariant. For example, “I am not the Pope” is an invariant of this loop, but it is not a useful one. A useful loop invariant is one that helps in proving some property of the program.

Here, presumably, the ultimate point of the exercise is to determine the return value of the function (as a function of the arguments a and b). The only way this function can return is on normal exit of the while loop, returning a in a state of the program where the condition a >= 0 and b >= 0 is false.

The property a >= b isn't likely to be relevant because it's neither true at the start of the function nor when the function returns.

Given the objective to figure out the value of a when the loop exits, it is useful to look at what happens in the last iteration of the loop. We know that a >= 0 and b >= 0 is true on entry to the function, so there will be at least one loop iteration. Let $a'$ and $b'$ be the values of a and b at the start of the last iteration, and $a''$ and $b''$ the values at the end. We know from the loop condition that $a' \ge 0$, $b' \ge 0$, and $a'' \lt 0 \vee b'' \lt 0$. This can only happen when the else branch is taken. Therefore $a'' = a' - 1$ and $b'' = b'$. Plugging these equalities into the inequalities we had, we get that $b'' \ge 0$ so $a'' \lt 0$ and also $a'' \ge -1$.

It appears that b >= 0 and a >= -1 are two invariants of the loop — they're true on entry and they're true on return. Furthermore, if the initial values of a and b are integers, the property “a and b are integers” are also loop invariants. If a and b are integers, then the only possible value for $a''$ given the inequalities above is $-1$, so this function can only return the value $-1$.

Follow-up exercices:

1. If a and b aren't constrained to be integers, what does the function return? You'll need to find another invariant to determine the value of $a''$.
2. If a and b are nonnegative integers, I've proved that this function can only return the value -1. I haven't proved that this function is equivalent to return -1, however: it might also loop infinitely. Prove that (given the precondition that the arguments are non-negative) the function always terminates.