Axiomatic Definitions of Programming Languages
Albert R. Meyer, Joseph Yehuda Halpern · Journal of the ACM · 1982
A precise defmttion is given of how partial correctness or termination assertions serve to define the semantics of program schemes Assertions involving only formulas of f'trst-order predicate calculus are proved capable of defining program scheme semanUcs, and effective ax,om systems for deriving such assertions are described.Such axiomatic definitions are possible despite the limited expressive power of predicate calculus.