Some classes of naturally provable programs

摘要

Three different classes of programs are identified for which the proof of correctness is shown to be "natural", in that the functional input-output specifications of the programs lead, in a straightforward manner, to the verification conditions that should be proven. Furthermore, these verification conditions are shown to be necessary and sufficient so that a proof/refutation follows by proving/disproving the corresponding verification conditions. It is not necessary to follow the exact control flow of the programs to generate these conditions; certain simple checks are enough to show whether a particular program belongs to one of the classes. These apparently different programs have the common feature that they operate "uniformly" on the data domain; changing the input to the program changes the dynamic behavior of the program in a predictable, easily definable fashion. Implications of this feature in program construction are discussed.