Proving programs correct: Some techniques and examples

Proving the correctness of computer programs is justified as both advantageous and feasible. The discipline of proof provides a systematic search for errors, and a completed proof gives sufficient reasons why the program must be correct. Feasibility is demonstrated by exhibiting proofs of five pieces of code. Each proof uses one or more of the illustrated proof techniques of case analysis, assertions, mathematical induction, standard prose proof, sectioning and a table of variable value changes. Proofs of other programs, some quite lengthy, are cited to support the claim that the techniques work on programs much larger than the examples of the paper. Hopefully, more programmers will be encouraged to prove programs correct.