##
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.