Weakest expressible preconditions: A new tool for proving completeness results about Hoare calculi

1. Bergstra, J.A. and Tucker, J.V.: Expressiveness and the completeness of Hoare's logic, Internal Report IW 149, Mathematisch Centrum Amsterdam (1980).

   Google Scholar 

2. Clarke, E.M., German, S.M. and Halpern, J.Y.: On effective axiomatizations of Hoare logics, 9th ACM Symp. on Principles of Programming Languages, 309–321 (1982).

   Google Scholar 

3. Cook, S.A.: Soundness and completeness of an axiomatic system for program verification, SIAM Journal of Computing 7, 1, 70–90 (1978).

   Google Scholar 

4. Manna, Z.: Mathematical theory of computation, Mc Graw-Hill 1974.

   Google Scholar 

5. Wand, M.: A new incompleteness result for Hoare's system, JACM 25, 168–175 (1978).

   Google Scholar 

Download references