97 Things Every Programmer Should Know

Chapter 15. Coding with Reason

Yechiel Kimchi

TRYING TO REASON about software correctness by hand results in a formal proof that is longer than the code, and more likely to contain errors. Automated tools are preferable but not always possible. What follows describes a middle path: reasoning semiformally about correctness.

The underlying approach is to divide all the code under consideration into short sections—from a single line, such as a function call, to blocks of less than 10 lines—and argue about their correctness. The arguments need only be strong enough to convince your devil’s advocate peer programmer.

A section should be chosen so that at each endpoint, the state of the program (namely, the program counter and the values of all “living” objects) satisfies an easily described property, and so that the functionality of that section (state transformation) is easy to describe as a single task; these guidelines will make reasoning simpler. Such endpoint properties generalize concepts like preconditions and postconditions for functions, and invariants for loops and classes (with respect to their instances). Striving for sections to be as independent of one another as possible simplifies reasoning and is indispensable when these sections are to be modified.

Many of the coding practices that are well known (although perhaps less well followed) and considered “good” make reasoning easier. ...