Axiomatic Definitions of Programming Languages: A Theoretical Assessment

Abstract

A precise definition is given of how partial correctness or termination assertions serve to specify the semantics of classes of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of specifying program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic specifications are possible despite the limited expressive power of predicate calculus.