Hoare's logic for programming languages with two data types

DOI10.1016/0304-3975(83)90072-5zbMath0522.68012OpenAlexW2135751232MaRDI QIDQ1056220

J. V. Tucker, 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/1865

zbMATH Keywords

completenessexpressivenesspartial correctnessHoare's logicwhile-programsmany-sorted first-order logicmany-sorted programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Data structures (68P05) General topics in the theory of software (68N01)

Related Items

Expressiveness and the completeness of Hoare's logic ⋮ The axiomatic semantics of programs based on Hoare's logic ⋮ Weakly expressive models for Hoare logic

Cites Work

• Expressiveness and the completeness of Hoare's logic
• Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• Another incompleteness result for Hoare's logic
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item