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

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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