In some sorts of code, you can get a lot of mileage from "loop invariants" and "loop variants". Understanding these is more or less the same as understanding pr

In some sorts of code, you can get a lot of mileage from "loop invariants" and "loop variants". Understanding these is more or less the same as understanding proof by induction. Whether you are missing anything depends on whether you ever write the sort of code that benefits from this. (Even if you do, you still might not be missing anything. You might be comfortable with loop invariants but not have connected them with proof by induction. Or you might be good at reasoning about these things in other ways that don't involve invariants.) (You can stop reading here if you're already very familiar with loop variants and invariants.) Here's the sort of thing I mean by loop variants/invariants. Suppose you're writing a binary search. (Don't write a binary search. Use someone else's that's already had the bugs taken out.) This is basically pretty simple but surprisingly easy to get subtly wrong, which means it's the sort of code it may be useful to write and document in such a way that you have an informal proof of its correctness. Like this: function find(a, x): # find x in sorted array a; return index i such that a[i]==x # or -1 if no such index exists. Takes time at most # proportional to log(#elements). lo,hi = a.index_bounds() while lo<hi: # INVARIANT: min index <= lo < hi <= max index+1 # INVARIANT: if x is in the array then lo <= its index < hi # VARIANT: D := hi-lo reduces to at most D/2 next iteration mid = lo + floor((hi-lo)/2) # may equal lo, can't equal hi if a[mid] == x: return mid # done! if a[mid] < x: lo = mid+1 else: hi = mid # INVARIANT: if x is in the array then lo <= its index < hi # now lo >= hi which means there's nowhere for x to live return -1 The above is pseudocode in no particular language. Is it correct? Those variants and invariants (1) divide that question in two and (2) provide a strategy for answering the second half of the question. First sub-question: if the (in)variants always hold, does that imply that the code is correct? Second sub-question: do they always hold? (Strategy for second sub-question: proof by induction on array size and/or number of iterations.) The first invariant implies that since mid is always between lo (inclusive) and hi (exclusive) it's safe to access a[mid]. The second, given that it holds at both start and end of the loop body, implies that if we exit the loop then indeed x isn't in the array. The only ways to leave the function are via the return in the middle, which only happens when we have explicitly found x, and via the return at the end, which only happens when x is known to be absent; therefore, if we return anything, we return the right thing. And the variant says that the quantity D, which starts by equalling the number of elements in the array, is reduced by a factor of at least 2 at each step; as it's always a (strictly) positive integer, this implies that the number of steps is at most log_2(n), so the function does return. (Note that that last bit is more or less a proof by induction on array size that the function always returns.) So if the invariants hold then the function does the right thing in the right amount of time. Proving that the invariants hold is the induction-like bit. The first invariant holds at the start (since lo,hi start out being exactly min index and max index + 1). Each time around the loop we replace either lo or hi with something in between the two, so we still have min <= lo <= hi < max+1; and we will exit the loop unless in fact lo<hi. So the first invariant always holds. The second invariant holds at the start (since lo,hi are bounds on the entire array). Because the array is sorted, our adjustments to lo/hi make this invariant true again for the next time around the loop. So the second invariant holds at the end of the loop -- and of course therefore at the start of the next iteration. (Note that those were both proofs by induction, though I wasn't super-explicit about the fact.) The variant works because if we write D = hi-lo and E = floor(D/2) then the new value of D is, depending on which branch of that if we take, either E or D-E-1; note that D-E-1<=E; so new-D <= E <= D/2 as claimed. It's probably pretty clear what sort of code this is useful for: highly "algorithmic" code that's basically doing something fairly simple but that's tricky to think about and easy to get wrong. If you're writing a language's standard library, or implementing some sort of iterative mathematical algorithm, then you're quite likely to find it useful. The less like that your code is, the less often this technique will be useful to you. (Fairly extreme example: if you are writing a CRUD webapp then it is unlikely that anything you do will benefit from this.)