Floyd-hoare logic in iteration theories

Stephen L. Bloom, Z. Ésik

Research output: Contribution to journalArticle

15 Citations (Scopus)

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 languageEnglish
Pages (from-to)887-934
Number of pages48
JournalJournal of the ACM
Volume38
Issue number4
Publication statusPublished - 1991

Fingerprint

Boolean algebra
Chemical analysis

Keywords

  • Correction assertions
  • Hoare logic

ASJC Scopus subject areas

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

Cite this

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

In: Journal of the ACM, Vol. 38, No. 4, 1991, p. 887-934.

Research output: Contribution to journalArticle

Bloom, SL & Ésik, Z 1991, 'Floyd-hoare logic in iteration theories', Journal of the ACM, vol. 38, no. 4, pp. 887-934.
Bloom, Stephen L. ; Ésik, Z. / Floyd-hoare logic in iteration theories. In: Journal of the ACM. 1991 ; Vol. 38, No. 4. pp. 887-934.
@article{ffe045811c3446adb3b0d4fa9cb72fd8,
title = "Floyd-hoare logic in iteration theories",
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.",
keywords = "Correction assertions, Hoare logic",
author = "Bloom, {Stephen L.} and Z. {\'E}sik",
year = "1991",
language = "English",
volume = "38",
pages = "887--934",
journal = "Journal of the ACM",
issn = "0004-5411",
publisher = "Association for Computing Machinery (ACM)",
number = "4",

}

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 -