Readable Proofs in Hoare Logic (and Separation Logic)

John C. Reynolds

If program verification, particularly machine-aided verification, is to become a useful tool for the programmer, it is vital to devise notations for proofs that are easily readable yet sufficiently formal to be mechanized.

It has become customary to describe proofs in Hoare logic informally by means of "annotated specifications" or "proof outlines". For simple programs, these annotated specifications are essentially similar to the annotated flowcharts introduced by Floyd and Naur, and they can be formalized (in particular, one can determine whether there are enough intermediate assertions) by using weakest preconditions. But weakest-precondition reasoning does not scale well, and breaks down in the presence of procedures or concurrency.

In fact, particularly in separation logic, it is useful to introduce enriched notation to deal with procedures, concurrency, and various structural rules such as the frame axiom.

Our goal is to insure that enriched annotated specifications actually determine valid formal proofs (modulo the correctness of verification conditions), while providing as much flexibility as possible. For this purpose, we give inference rules for judgements called "annotation definitions", that assert that an annotated specification determines a particular Hoare triple.