The axiomatic semantics of programs based on Hoare's logic
Jan Aldert Bergstra, Judith Tucker · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1983
This paper is about the Floyd-Hoare Principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language.We study the simple language WP of while-programs and Hoare' s system for partial correctness and we calculate the semantics of WP as this is determined by Hoare' s logic.This calculation is possible by using relational semantics to build a completeness theorem for the logic.The resulting semantics AX we call the axiomatic semantics for WP.This AX is not the conventional semantics for WP : it need not be effectively computable or deterministic, for example.A large number of elegant properties of AS are proved and the Floyd-Hoare Principle is reconsidered.