Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs

DOI10.1016/0304-3975(82)90027-5zbMath0483.68033OpenAlexW2164256202MaRDI QIDQ1163369

J. V. Tucker, Jan A. Bergstra

Publication date: 1982

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

Full work available at URL: https://dspace.library.uu.nl/handle/1874/12713

zbMATH Keywords

halting problemPresburger arithmeticHoare's logicincompleteness partial correctnesstheories of algebraically and real closed fields

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25)

Related Items

Some general incompleteness results for partial correctness logics, Hoare's logic and Peano's arithmetic, Fifty years of Hoare's logic, Two theorems about the completeness of Hoare's logic, Expressiveness and the completeness of Hoare's logic, The axiomatic semantics of programs based on Hoare's logic, Some questions about expressiveness and relative completeness in Hoare's logic, Weakly expressive models for Hoare logic

Cites Work

• Expressiveness and the completeness of Hoare's logic
• Floyd's principle, correctness theories and program equivalence
• On procedures as open subroutines. II
• Theory of program structures: Schemes, semantics, verification
• Recursive assertions are not enough - or are they?
• A note on computable real fields
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• A Complete and Consistent Hoare Axiomatics for a Simple Programming Language
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• 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