Expressiveness and the completeness of Hoare's logic

Other nonclassical logic (03B60) Categoricity and completeness of theories (03C35) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

The authors prove three theorems about completeness issues regarding Hoare's logic for while-programs: (1) expressiveness is not a necessary condition on a structure for the completeness of its Hoare logic, (2) complete number theory is the only extension of Peano Arithmetic which yields a logically complete Hoare logic and (3) a computable structure with enumeration is expressive iff its Hoare logic is complete. Here expressiveness means the ability of expressing strongest postconditions in first-order formulas over the structure concerned; a Hoare logic H is called complete relative to a structure A if any partial correctness formula valid over A is provable in H, where facts about A can be used as an oracle; a Hoare logic H is called logically complete with respect to a specification (theory) T if any partial correctness formula that is valid on all models of T is provable in H. The authors conclude from (1) that in general Cook's analysis of the completeness of Hoare logic is not sufficient, but also that by (3), in the most interesting cases in which computable structures are involved, Cook's notion of expressiveness is enough for the study of completeness. Since for every finite structure expressiveness is guaranteed, their Hoare logics are always complete. Moreover, for every infinite computable structure it is proved to be possible to enrich the signature, such that expressiveness becomes equivalent to completeness of the Hoare logic relative to the enriched structure. However, it is still an open problem whether this also holds in general for the original (infinite computable) structure. Finally a note on the use of Lemma 4.5 in the proof of Theorem 4.3 on p. 277: the three bottom lines have to be replaced by: From Lemma 4.5 and II(d) we obtain \(\vdash\neg \phi (x)\to\forall y(x\neq y).\)

Recommendations

Cites work

Cited in

(30)

This page was built for publication: Expressiveness and the completeness of Hoare's logic

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