### Abstract

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 {α}/{β} as an equation between iteration theory terms. The guards (α,β) 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 program-ming 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 conn ection with completeness is examined.

Original language | English |
---|---|

Pages (from-to) | 887-934 |

Number of pages | 48 |

Journal | Journal of the ACM |

Volume | 38 |

Issue number | 4 |

Publication status | Published - 1991 |

### Fingerprint

### Keywords

- Correction assertions
- Hoare logic

### ASJC Scopus subject areas

- Hardware and Architecture
- Software
- Artificial Intelligence
- Information Systems
- Control and Systems Engineering

### Cite this

*Journal of the ACM*,

*38*(4), 887-934.

**Floyd-hoare logic in iteration theories.** / Bloom, Stephen L.; Ésik, Z.

Research output: Contribution to journal › Article

*Journal of the ACM*, vol. 38, no. 4, pp. 887-934.

}

TY - JOUR

T1 - Floyd-hoare logic in iteration theories

AU - Bloom, Stephen L.

AU - Ésik, Z.

PY - 1991

Y1 - 1991

N2 - 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 {α}/{β} as an equation between iteration theory terms. The guards (α,β) 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 program-ming 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 conn ection with completeness is examined.

AB - 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 {α}/{β} as an equation between iteration theory terms. The guards (α,β) 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 program-ming 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 conn ection with completeness is examined.

KW - Correction assertions

KW - Hoare logic

UR - http://www.scopus.com/inward/record.url?scp=0000860669&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0000860669&partnerID=8YFLogxK

M3 - Article

VL - 38

SP - 887

EP - 934

JO - Journal of the ACM

JF - Journal of the ACM

SN - 0004-5411

IS - 4

ER -