Chapter 15. Coding with Reason
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 ...
Get 97 Things Every Programmer Should Know now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.