A New Incompleteness Result for Hoare's System
From MaRDI portal
Publication:4139636
DOI10.1145/322047.322062zbMath0364.68008OpenAlexW1994586366MaRDI QIDQ4139636
Publication date: 1978
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322047.322062
Related Items (21)
The semantics of Hoare's iteration rule ⋮ Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming ⋮ Some general incompleteness results for partial correctness logics ⋮ A methodology for designing proof rules for fair parallel programs ⋮ A language independent proof of the soundness and completeness of generalized Hoare logic ⋮ Unnamed Item ⋮ Semantical analysis of specification logic ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ On the completeness of modular proof systems ⋮ A mechanical analysis of program verification strategies ⋮ Proof methods of declarative properties of definite programs ⋮ Fifty years of Hoare's logic ⋮ Recursive assertions are not enough - or are they? ⋮ Current methods for proving program correctness ⋮ Generating algebraic laws from imperative programs ⋮ Proving program inclusion using Hoare's logic ⋮ Average case optimality for linear problems ⋮ Expressiveness and the completeness of Hoare's logic ⋮ Some questions about expressiveness and relative completeness in Hoare's logic ⋮ Weakly expressive models for Hoare logic ⋮ On the mechanical derivation of loop invariants
This page was built for publication: A New Incompleteness Result for Hoare's System