Floyd-Hoare logic in iteration theories
Stephen L. Bloom, Zoltán Ésik · Journal of the ACM · 1991
What is special about the rules of Hoare logic?This paper shows that partial correctness logic can be viewed as a special case of the equational logic of iteration theories [6,7,24].It is shown how to formulate a partial correctness assertion {a} f { /3} as an equation between iteration theory terms.The guards (a, ~) that appear in partial correctness assertions are equationally axiomatized, and a new representation theorem for Boolean algebras is derived.The familiar rules for the structured programming constructs of composition, if-then-else and while-do are shown valid in all guarded iteration theories.A new system of partial correctness logic is described that applies to all flowchart programs.The invariant guard condition, weaker than the well-known condition of expressiveness.is found to be both necessary and sufficient for the completeness of these rules.The Cook completeness theorem [19] follows as an easy corollary.The role played by weakest liberal preconditions in connection with completeness is examined.