I Remember Loop Invariants

Apparently all models of the 30GB Microsoft Zune music player failed yesterday, New Year's Eve.  The cause, as revealed here, was a bug in the C code that will put the Zune processor into a closed loop on day 366 of any leap year.  Reading the Microsoft code (a more complete listing is here), and the attempts to fix it here, made me realize that there are still programmers who do not understand loop invariants (at least not well enough to be able to use them when they need to).  Sigh.  I can still remember the excitement I felt when I first read about them back in 1983: no longer did I have to have to try to understand code by stepping through it, one instruction at a time, or by just staring at it very hard; instead I had a systematic way of laying out the underlying structure of the problem that was to be solved, and then deriving the code from it.  Even if you don't use loop invariants formally, they are an incredibly useful tool for clarifying your thinking on the more difficult bits of code.