Some questions about expressiveness and relative completeness in Hoare's logic

DOI10.1016/0304-3975(85)90138-0zbMath0575.68015OpenAlexW2073711304MaRDI QIDQ1064046

Mario Rodríguez Artalejo

Publication date: 1985

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

Full work available at URL: https://doi.org/10.1016/0304-3975(85)90138-0

zbMATH Keywords

Hoare's logicwhile-programsexpressive structurepartial correctness assertion

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

Recursive programs and denotational semantics in absolute logics of programs, Some general incompleteness results for partial correctness logics, Hoare's logic for nondeterministic regular programs: A nonstandard approach, Weakly expressive models for Hoare logic

Cites Work

• Expressiveness and the completeness of Hoare's logic
• A complete logic for reasoning about programs via nonstandard model theory. II
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Definability by programs in first-order structures
• Model theory
• On the notion of expressiveness and the rule of adaptation
• Ten Years of Hoare's Logic: A Survey—Part I
• The unwind property in certain algebras
• On the termination of program schemas
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item