Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer

Abstract

We consider three kinds of mathematical objects which can be designated as the “meaning” or “semantics” of programs: binary relations between initial and final states, binary relations on predicates (partial-correctness semantics), and functionals from predicates to predicates (predicate transformers). We exhibit various formal specification mechanisms: induction on program syntax, axioms, and deductive systems. We show that each kind of semantics can be specified by several different mechanisms. As long as arbitrary predicates on states are permitted, each kind of semantics uniquely determines the others, with the sole exception of the weakest precondition semantics for nondeterministic programs. © 1981, ACM. All rights reserved.