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

DOI10.1016/0304-3975(82)90027-5MaRDI QIDQ1163369zbMATH OpenOpenAlexFDO

Authors John V. Tucker, J. 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 problemHoare's logicincompleteness partial correctnessPresburger arithmetictheories of algebraically and real closed fields

Mathematics Subject Classification ID

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

Cites work

• A Complete and Consistent Hoare Axiomatics for a Simple Programming Language
• A New Incompleteness Result for Hoare's System
• A note on computable real fields
• An axiomatic basis for computer programming
• Computable Algebra, General Theory and Theory of Computable Fields
• CONSTRUCTIVE ALGEBRAS I
• Expressiveness and the completeness of Hoare's logic
• Floyd's principle, correctness theories and program equivalence
• scientific article; zbMATH DE number 3645075 (Why is no real title available?)
• scientific article; zbMATH DE number 3664338 (Why is no real title available?)
• scientific article; zbMATH DE number 3683035 (Why is no real title available?)
• scientific article; zbMATH DE number 3688676 (Why is no real title available?)
• scientific article; zbMATH DE number 3688693 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3597842 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3315195 (Why is no real title available?)
• scientific article; zbMATH DE number 3316928 (Why is no real title available?)
• On procedures as open subroutines. II
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Recursive assertions are not enough - or are they?
• Soundness and Completeness of an Axiom System for Program Verification
• Theory of program structures: Schemes, semantics, verification

Cited in

(8)

• Some questions about expressiveness and relative completeness in Hoare's logic
• 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
• Weakly expressive models for Hoare logic

This page was built for publication: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs

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