Attempts to prove the correctness of software manually lead to a formal proof that is longer than the code itself and contains errors more frequently than the code. It is preferable to use automated tools, but this is not always possible. Below, a middle ground is described: semi-formal proof of correctness.
The method is based on dividing the code under investigation into short fragments ranging from a single line, which may contain a function call, to blocks no longer than 10 lines, and discussing their correctness. The proof must be convincing enough for your colleague playing the role of the “devil’s advocate.”
Fragments should be chosen in such a way that at the end point of the block, the program state (namely, the instruction address counter and the values of all “live” objects) satisfies a property that is simple to describe, and the functionality of this fragment (state transformation) can be easily described as a single independent task. Adhering to the proposed rules simplifies the proof process. Such properties of the fragment’s endpoint generalize the concepts of preconditions and postconditions for functions, as well as invariants for loops and classes (with respect to class instances). It is necessary to strive for fragments to be as independent from each other as possible, which facilitates proof and will be very useful if these fragments are to be modified.
Many well-known (although apparently less frequently applied) and recognized as “high-quality” coding practices also facilitate the process of conducting proofs. Thus, the mere intention to prove the correctness of one’s code in the future contributes to improving its style and structure. It is not surprising that most of these practices are checked by static code analyzers:
- Avoid goto statements because they create strong dependencies between fragments that are spread throughout the code. - Avoid mutable global variables because they make all fragments that use them dependent on each other. - The scope of each variable should be the smallest possible. For example, a local object can be declared immediately before its first use. - Make objects immutable where possible. - Improve code readability through spaces – both horizontal and vertical. For example, align the indents for related structures and separate code fragments with blank lines. - Write self-documenting code by choosing meaningful (but sufficiently short) names for objects, functions, types, etc. - If the fragment turns out to be nested, turn it into a function. - Each function should solve a single task and be short. The 24-line function length limit, introduced many years ago, still applies. The size and resolution of screens compared to the 1960s have increased, but human perception capabilities remain the same. - A function should not have many arguments (a good practice is no more than four). This does not limit the amount of data passed to the function: combining related arguments into a single object localizes the object’s invariants, which simplifies the proof in terms of checking the consistency and states of the objects. - In general, each unit of code, from a fragment to an entire library, should have a limited interface. Reducing the flow of information simplifies the proof. This means that methods returning internal state (getters) should be avoided. You should not request information from the object for processing, but rather demand that it perform the work with the information it already has. In other words, encapsulation is limited interfaces, and only those. - To preserve class invariants, one should avoid methods that assign values (setters). They often lead to violations of the invariants that define the object’s states.
Proving the correctness of the code, as well as discussing it, will help you understand it better. Share your findings – it will benefit everyone.