The axiomatic semantics of programs based on Hoare's logic

DOI10.1007/BF00264252zbMATH Open0551.68016MaRDI QIDQ800712FDOQ800712

Authors: John V. Tucker, J. A. Bergstra 

Publication date: 1984

Published in: Acta Informatica (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 4058826
• Towards reasoning about Hoare relations
• scientific article; zbMATH DE number 3848601
• Two theorems about the completeness of Hoare's logic
• The semantics of Hoare's iteration rule

zbMATH Keywords

programming languagesemanticsaxiomatic relational semanticscorrectness of programsFloyd-Hoare principlewhile-programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Expressiveness and the completeness of Hoare's logic
• Guarded commands, nondeterminacy and formal derivation of programs
• CONSTRUCTIVE ALGEBRAS I
• Computable Algebra, General Theory and Theory of Computable Fields
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An axiomatic definition of the programming language Pascal
• Title not available (Why is that?)
• A complete logic for reasoning about programs via nonstandard model theory. I
• Proof rules for the programming language Euclid
• 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 and Peano's arithmetic
• Consistent and complementary formal theories of the semantics of programming languages
• Two theorems about the completeness of Hoare's logic
• Hoare's logic for programming languages with two data types
• Infinite proof rules for loops
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Axiomatic Definitions of Programming Languages
• Title not available (Why is that?)

Cited In (17)

• The B-Book
• Some general incompleteness results for partial correctness logics
• Dijkstra's interpretation of the approach to solving a problem of program correctness
• Title not available (Why is that?)
• Matching logic: an alternative to Hoare/Floyd logic
• Algebraic specifications of computable and semicomputable data types
• AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• Title not available (Why is that?)
• Indexed and fibered structures for partial and total correctness assertions
• Forward with Hoare
• Axiomatization of if-then-else over possibly non-halting programs and tests
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Title not available (Why is that?)
• Title not available (Why is that?)
• A complete axiomatic semantics of spawning
• The semantics of Hoare's iteration rule

Uses Software

• ALGOL 68

This page was built for publication: The axiomatic semantics of programs based on Hoare's logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q800712)