Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

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.

share|improve this question
add comment

1 Answer 1

up vote 8 down vote accepted

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.