On the inadequacy of ordinary preconditions for the practical design and verification of programs

A mathematical basis for verifying computer programs has existed for some time but is used in practice only relatively infrequently. One of the reasons often cited for this lack of acceptance is that the proposed approaches fail to address certain questions of practical importance, e.g. whether a program even executes successfully or not. The commonly propounded proof rules do not deal with “run time” errors. While such considerations can be brought into a formal analysis of program correctness, previously proposed methods add extra steps and significant complexity to the process or are at least perceived by many to do so. Traditional approaches to program correctness distinguish between partial and total correctness. Very frequently the only difference between them is the consideration of whether loops terminate or not. This is not sufficient in practice, where the failure of even a simple assignment statement to execute must be considered. Three levels of correctness are required: partial correctness (as defined traditionally), semi-strictly total correctness and strictly total correctness. Semi-strictly total correctness guarantees that each individual statement in the program executes with a defined result (no “run time” errors) but permits loops (and recursive calls) to execute indefinitely. Strictly total correctness guarantees in addition that execution of the entire program terminates. The paper presents straightforward extensions to traditional proof rules for semi-strict and strict preconditions