On proving the absence of execution errors
W. David Elliott · 1980
An important and neglected program property is that the program executes cleanly, that is, without execution errors such as dividing by zero, referencing an uninitialized variable, or aliasing. The language designer has lacked a precise way of specifying when execution errors occur, and the language user good means of proving they will not occur. This thesis provides a method for formally defining conditions that ensure the absence of execution errors. Using rewrite rules based on a grammar for the programming language in question, a sufficient condition can be defined for each construct in the language that ensures the absence of execution errors for that construct. Applied to a program segment, the rewrite rules produce the corresponding clean execution condition. Clean execution conditions cannot be defined using rewrite rules alone for statement sequences, declarations composed with their associated scopes, and parameterized declarations (procedure and function declarations, loops, and parameterized types). The rewrite rule approach is extended to handle these constructs using predicate transformers, substitution functions, and inference rules (together with pre/postcondition descriptions) respectively. The approach is illustrated on a Pascal-based language; the clean execution of much of the programming languaged Euclid is defined in an appendix. In addition to providing a method for formally defining conditions that ensure the absence of execution errors, and thus providing a formalism that allows more complete language definition, the method provides a notation for documenting language design decisions about execution constraints, a discipline for considering clean execution during language design, and better means for verifying clean execution.