Proving program inclusion using Hoare's logic

DOI10.1016/0304-3975(84)90065-3zbMath0533.68011OpenAlexW2150726636MaRDI QIDQ789887

Jan Willem Klop, Jan A. Bergstra

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/1833

zbMATH Keywords

program correctnessprogram equivalenceconservative refinementdata type specificationlogical completionprototype proof

Mathematics Subject Classification ID

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

Related Items

Hoare's logic for nondeterministic regular programs: A nonstandard approach

Cites Work

• Two theorems about the completeness of Hoare's logic
• Expressiveness and the completeness of Hoare's logic
• Correctness of the compiling process based on axiomatic semantics
• 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
• How to Program an Infinite Abacus
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• 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
• Unnamed Item
• Unnamed Item