Program Proving: Exit and Return Jumps in Structured Programs

Abstract

The inadequacy of goto-free programming languages to express algorithms has clearly been shown in the literature. On the other hand, the axiomatic definition of jumps is rather complex, and there aren’t complete or efficient proposals for it.

On the basis of Clint and Hoare’s semantical analysis of jump occurrences in structured programs, which leads to the distinction between return and exit jumps, a twofold solution to the above problem is presented in the present paper.

On the one hand, to express return jumps (considered as belonging to the normal computation flow of the algotithm), iterative one-level exit constructs wider than the simple iteration (do-while like) statement are considered, and the related correctness rules are given. On the other hand, a limited form of goto statement is introduced, with which an explicit definition of the jump condition is associated, restricted to deal with the case of exit jump only (considered as expressing exceptions in the program)

The jump condition is then used to prove the ‘almost everywhere correctness’ of the normal computation flow of the program, ignoring the exit jumps, whose correctness can be dealt with separately.

Examples of the above constructs and correctness rules and of an ‘almost everywhere correctness’ proof, are given.