Expressiveness and the completeness of Hoare's logic

DOI10.1016/0022-0000(82)90013-7zbMath0549.68021OpenAlexW1975577974MaRDI QIDQ800082

J. V. Tucker, Jan A. Bergstra

Publication date: 1982

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://dspace.library.uu.nl/handle/1874/13392

zbMATH Keywords

completenessexpressivenesscomputable structurescomplete number theorycomputable data structuresHoare's logic for while- programs

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Categoricity and completeness of theories (03C35)

Related Items (18)

The verification of modules ⋮ Completeness for recursive procedures in separation logic ⋮ Algebraic specifications of computable and semicomputable data types ⋮ Some general incompleteness results for partial correctness logics ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Completeness of Hoare logic with inputs over the standard model ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Semantical analysis of specification logic ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ Fifty years of Hoare's logic ⋮ On the notion of expressiveness and the rule of adaptation ⋮ Proving program inclusion using Hoare's logic ⋮ Hoare's logic for programming languages with two data types ⋮ Average case optimality for linear problems ⋮ The axiomatic semantics of programs based on Hoare's logic ⋮ Some questions about expressiveness and relative completeness in Hoare's logic ⋮ Weakly expressive models for Hoare logic

Cites Work

• Hoare's logic for programming languages with two data types
• Floyd's principle, correctness theories and program equivalence
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Theory of program structures: Schemes, semantics, verification
• Model theory
• An axiomatic definition of the programming language Pascal
• Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
• A New Incompleteness Result for Hoare's System
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• CONSTRUCTIVE ALGEBRAS I
• Computable Algebra, General Theory and Theory of Computable Fields
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Expressiveness and the completeness of Hoare's logic