The axiomatic semantics of programs based on Hoare's logic
From MaRDI portal
Publication:800712
DOI10.1007/BF00264252zbMath0551.68016MaRDI QIDQ800712
Publication date: 1984
Published in: Acta Informatica (Search for Journal in Brave)
semanticsprogramming languagecorrectness of programsaxiomatic relational semanticsFloyd-Hoare principlewhile-programs
Related Items
Algebraic specifications of computable and semicomputable data types ⋮ Some general incompleteness results for partial correctness logics ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach
Uses Software
Cites Work
- Two theorems about the completeness of Hoare's logic
- Expressiveness and the completeness of Hoare's logic
- Hoare's logic for programming languages with two data types
- Infinite proof rules for loops
- Floyd's principle, correctness theories and program equivalence
- A complete logic for reasoning about programs via nonstandard model theory. I
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
- Hoare's logic and Peano's arithmetic
- Proof rules for the programming language Euclid
- An axiomatic definition of the programming language Pascal
- Consistent and complementary formal theories of the semantics of programming languages
- A PROPERTY OF 2‐SORTED PEANO MODELS AND 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
- Axiomatic Definitions of Programming Languages
- Guarded commands, nondeterminacy and formal derivation of programs
- Soundness and Completeness of an Axiom System for Program Verification
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
