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.
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.
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.
[+] [-] mjcohen|11 years ago|reply
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.
[+] [-] NhanH|11 years ago|reply
[+] [-] 27182818284|11 years ago|reply
I'm curious. Is this like a "supper vs dinner" or "pop vs soda" variation that depends on the region your university is located?
[+] [-] vilhelm_s|11 years ago|reply
[1] http://cstheory.stackexchange.com/questions/1521/origins-and...
[+] [-] Roboprog|11 years ago|reply
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 :-(
[+] [-] toolslive|11 years ago|reply
[+] [-] dill_day|11 years ago|reply
[+] [-] ksikka|11 years ago|reply