Expressiveness and the completeness of Hoare's logic
DOI10.1016/0022-0000(82)90013-7zbMATH Open0549.68021OpenAlexW1975577974MaRDI QIDQ800082FDOQ800082
Authors: John V. Tucker, J. 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
Recommendations
completenessexpressivenesscomputable structurescomplete number theorycomputable data structuresHoare's logic for while- programs
Other nonclassical logic (03B60) Specification and verification (program logics, model checking, etc.) (68Q60) Categoricity and completeness of theories (03C35) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Model theory
- An axiomatic basis for computer programming
- Ten Years of Hoare's Logic: A Survey—Part I
- CONSTRUCTIVE ALGEBRAS I
- Computable Algebra, General Theory and Theory of Computable Fields
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theory of program structures: Schemes, semantics, verification
- An axiomatic definition of the programming language Pascal
- A New Incompleteness Result for Hoare's System
- Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
- Floyd's principle, correctness theories and program equivalence
- Hoare's logic for programming languages with two data types
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
Cited In (30)
- Expressive power and incompleteness of propositional logics
- The verification of modules
- Title not available (Why is that?)
- Some general incompleteness results for partial correctness logics
- Title not available (Why is that?)
- Completeness for recursive procedures in separation logic
- Semantical analysis of specification logic
- Fifty years of Hoare's logic
- Completeness of Hoare logic relative to the standard model
- Algebraic specifications of computable and semicomputable data types
- Completeness and expressiveness of pointer program verification by separation logic
- Title not available (Why is that?)
- Average case optimality for linear problems
- Completeness of Hoare logic with inputs over the standard model
- Title not available (Why is that?)
- Expressive completeness and decidability
- First order Büchi automata and their application to verification of LTL specifications
- Title not available (Why is that?)
- On the completeness of propositional Hoare logic
- Title not available (Why is that?)
- Proving program inclusion using Hoare's logic
- Two theorems about the completeness of Hoare's logic
- The axiomatic semantics of programs based on Hoare's logic
- On the notion of expressiveness and the rule of adaptation
- Weakly expressive models for Hoare logic
- Hoare's logic for programming languages with two data types
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
- Some questions about expressiveness and relative completeness in Hoare's logic
- On relative completeness of Hoare logics
This page was built for publication: Expressiveness and the completeness of Hoare's logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q800082)
