I have a bit of experience with loop invariants but I'm not really clear on them. I'm trying to learn them through an example in Python. Can someone point one out or help me understand?
I've searched both on programmers.SX and on the web but the only things I could find were invariants and design by contract -- nothing on loop invariants.
A loop invariant is simply something that is true on every iteration of the loop. For example, take a really trivial while loop:
while x <= 5:
x = x + 1
Here the loop invariant would be that x ≤ 6. Obviously, in real life, loop invariants are going to be more complicated--finding the loop invariant in general is something of an art and cannot easily be done algorithmically (as far as I know).
So, why is this useful? Well, at a coarse level, it's good for debugging: if you identify an important invariant, it's easy to check that it holds even when you modify some code. You could just add an assert statement of some sort:
while x <= 5:
x = x + 1
assert x <= 6
More specifically, these invariants help us reason about how loops behave. This is where axiomatic semantics and Hoare logic come in. (This part of the answer is a little bit more advanced and esoteric, so don't worry about it too much.) Just in case you're rusty on notation: ⇒ means "implies", ∧ means "and" and ¬ means "not".
The basic idea is that we want a systematic way to prove properties of our code. The way we approach this is by looking at preconditions and postconditions in the code. That is, we want to prove that if some condition A holds before we run our code, some condition B holds after we run it. We generally write this as:
{A} code {B}
In general, this is pretty simple. You can intuitively figure out how to prove something like {x = 0} x = x + 1 {x = 1}. You can do this by substituting x + 1 for x in the postcondition, giving you a logic formula of x = 0 ⇒ x + 1 = 1 which is obviously true. This is how you deal with assignment in general: you just substitute the new value for the variable in the postcondition.
Other constructs like multiple statements in a row and if statements are pretty intuitive as well.
However, how do you do this for loops? That's a difficult question because you do not know (in general) how many times a given loop will iterate. This is where loop invariants come in. We are looking at a loop like:
while cond: code
There are two possibilities here. If cond is False, then it's trivial: the loop doesn't do anything, so we just get A ⇒ B. But what if the loop actually gets run? This is where we need the invariant.
The idea behind the invariant is that it always holds inside the loop. When you are inside the while loop, cond is always true. So we get an assertion like this:
{A ∧ cond} code {A}
This just writes out what we needed formally: given that A (the loop invariant) and cond hold at the beginning of the loop body, A has to hold at the end. If we can prove this for the loop body, we know that A will hold no matter how many times the loop executes. So, given the above statement is true, we can infer:
{A} while cond: code {A}
as an added bonus, since the while loop just finished, we know that cond has to be false. So we can actually write out the full result as:
{A} while cond: code {A ∧ ¬cond}
So lets use these rules to prove something about my example above. What we want to prove is:
{x ≤ 0} while x <= 5: x = x + 1 {x = 6}
That is, we want to show that if we start with a small x, at the end of the loop x will always be 6. This is pretty trivial, but it makes a good illustrative example. So the first step is to find a loop invariant. In this case, the invariant is going to be x ≤ 6. We now need to show that this is actually a loop invariant:
{x ≤ 5 ∧ x ≤ 6} x = x + 1 {x ≤ 6}
That is, if x is less than or equal to 5, x is less than or equal to 6 after running x = x + 1. We can do this using the substitution rule outlined above, but it's pretty obvious anyhow.
So, knowing this, we can infer the rule for the whole loop:
{x ≤ 6} while x <= 5: x = x + 1 {x ≤ 6 ∧ ¬(x ≤ 5)}
So this tells us that, at the end of the loop, x is both greater than 5 and less than or equal to 6. This simplifies to x = 6. Since x ≤ 6 whenever x ≤ 0, we've proved our initial statement.
Now, this might seem to be a lot of ostentation for proving something very obvious. After all, any programmer could have told you the value of x at the end of this loop! However, the important idea is that this method scales to more complicated loops which may not be immediately obvious. But if you can come up with an invariant for such a loop, you can use it to prove more interesting properties.
Anyhow, I hope that wasn't too confusing and gave you a good idea of why loop invariants are important at a more fundamental level.
I found a very good explanation, which includes an example of usage, here:
http://www.cs.uofs.edu/~mccloske/courses/cmps144/invariants_lec.html
The example with red and blue marbles in the jar totally explained the trick. I will try to summarise so that the answer complies with stack rules (some parts might be a copy-paste of the original).
-Suppose there is a jar and it contains a certain amount N of RED or BLUE marbles (N >=1).
-You also have an unlimited amount of RED marbles on the side.
PROCEDURE:
while (N > 1):
pick any two marbles from the jar
if (marbles have same colour):
remove marbles
put 1 RED marble in the jar
else: // marble have different colour
remove picked RED marble
put picked BLUE marble back
Examining this procedure you can see that N decreases by one at each iteration. So, if you know that at the beginning the jar contained N marbles, after N-1 loops it will contain only 1. This is an intuitive but informal argument that "loop terminates after finitely many iterations".
Suppose the amount of RED and BLUE marbles in the jar is initially known. Let's try to predict the colour of the last marble in the jar at the end of the procedure.
Formally, we are trying to find a function
f: N × N --> {BLUE, RED},
domain: set of ordered pairs of natural numbers,
range: is the set {BLUE, RED})
that satisfies the following condition:
For all K and M (such that at least one of them is non-zero),
if we begin with K RED marbles and M BLUE marbles in the jar,
then the last marble remaining in the jar is necessarily of color f(K,M).
The way to identify this function is to first find an invariant of the loop that works on the amount of BLUE marbles in the jar.
Considering one iteration of the loop and its effect on the number of BLUE marbles:
Case 1: both marbles have same colour:
subcase 1.1: marbles are BLUE (number of BLUE marble decreases by 2)
subcase 1.2: marbles are RED (number of BLUE marble stays the same)
Case 2: marbles have different colour: (number of BLUE marble stays the same)
We can appreciate how one single loop iteration has no effect on the parity of the number of BLUE marbles. M will remain odd or even (depending on the beginning state) as a result of the iteration.
This property will hold true for any number of iterations.
Let us denote:
Big_K the number of BLUE marbles in the jar at the beginning
small_k the number of BLUE marbles currently in the jar
then an invariant of the loop is:
small_k is odd if and only if Big_K is odd
This can be also expressed in a different way:
(both Big_K and small_k are odd) or (both Big_K and small_k are even)
Suppose the number of BLUE marbles initially in the jar, Big_K, were odd. "Recall that because a loop invariant holds at the end of every iteration, it holds, in particular, at the end of the last iteration."
Then the last marble in the jar must be BLUE, because otherwise small_k = 0 (even). Similarly, if Big_K were even, the last marble must be RED, because otherwise k = 1 (odd).
Function f is as follows:
f(Big_K,M) = { RED if Big_K is even
{ BLUE if Big_K is odd
all credit goes to Robert McCloskey http://www.cs.uofs.edu/~mccloske/ for his very helpful explanation on Loop Invariants
