Correctness proofs

A correctness proof is a formal mathematical argument that an algorithm meets its specification, which means that it always produces the correct out-put for any permitted input. Detailed correctness proofs of even moderately complex algorithms can be surprisingly long, so algorithms researchers (and writers of textbooks like [CLRS01]) often write informal arguments giving only an outline of the full proof. The relationship between the informal ar-gument and the underlying proof is analogous to the relationship between an informal definition of an algorithm and a program that implements it: the informal argument is only justified by being backed by an implicit formal proof that is sadly too long, unenlightening, or tiresome to present. So it is important to understand what a detailed formal correctness proof looks like, because otherwise you won’t know what somebody (possibly including you!) is really saying with an informal correctness argument. 1 Invariants, preconditions, and postconditions When viewed from a high enough level of abstraction, most correctnes