back
12 comments
If you are trying to prove (formally or informally) that a program is correct, loop invariants allow you to prove that loops do what you want. Contrapositively, if you can't write a loop invariant, you probably do not really understand what the loop is doing.

I have had Dijkstra's book for many years, and love it. It's a great read, and it should be reprinted or put into the public domain.

May I ask which Dijkstra's book you are referring to?
Probably A Discipline of Programming

http://www.alibris.com/A-Discipline-of-Programming-Edward-W-...

Interestingly, I had never heard the phrase "loop invariant" despite having taken math courses on proofs and a lower-level (300-level, quicksort, etc) algorithms course.

I'm curious. Is this like a "supper vs dinner" or "pop vs soda" variation that depends on the region your university is located?

Maybe? There is a sort of cultural split in theoretical computer science between "A theory" (algorithms and complexity) and "B theory" (logic/semantics/program verification).[1] And these in turn are sortof geographically divided, with complexity being popular in the US and logic in Europe. The concept of loop invariants comes from the program verification tradition, I guess it gets less emphasis when focusing on complexity.

[1] http://cstheory.stackexchange.com/questions/1521/origins-and...

I went to a little school in the CSU system in the 80s, but at least one of our professors used the term "loop invariant" (as well as induction) in our freshman "Pascal" class.

I admit I liked the recursive version of the author's example better, though, especially when he gets into "oldr" and "newr" to track the mutated state of things in each loop pass.

Along a similar line, I remember reading on my own about Eiffel and "class invariants" in the very early 90s.

Then came the internet gold rush to dumb things down, though. Now, we have King Java and its idiotic "bean" anti-pattern. Just make a useless crap object, whack on it enough (mutate it) until you hope it's in a useful state and slog onward! State of the art brain damage :-(

It used to be the standard way of teaching control structures. "so you want to write a 'while' loop? Then what's the invariant?". Also, the invariant is the best comment/documentation you can add to a complex loop.
I wouldn't guess so, for example it's used in the CLRS textbook. What did you call it instead?
I don't remember it ever being named. It isn't the same as the "inductive step" when learning proofs by induction, is it?
I understand your confusion, because the author didn't properly cover what he's talking about. It appears to be written to teach people who already know the material.

In the previous article, the closest thing to an explanation or definition of a loop invariant is, "We can make it less so by writing down a specific claim that applies to our particular loop. Such a claim is called a loop invariant." Not a very good description, and he doesn't try to do any better elsewhere.

I ended up having to do a bunch of googling after reading the articles to piece together what is trying to be explained, since I had never heard of loop invariants in that terminology either.

Simply put, a loop invariant is a condition or set of conditions that is true through the loop. This makes it akin to inductive proofs. The loop invariant must prove true for n and n+1 for it to be true for the entirety of the loop. Noting how similar this is to inductive reasoning, you can apply an inductive proof to a loop invariant to prove it.

The easiest way I've seen to explain it is in the body of the executing loop you ask yourself, "What has the loop done so far." An answer to that question should yield a loop invariant.

In the linked article, the author points to an explanation of loop invariants. Click the link "Last Week"
Relevant course notes from a course at Carnegie Mellon - http://www.cs.cmu.edu/~fp/courses/15122-s11/recitations/reci...