  Automatic program verification has made tremendous strides, but is not yet
for the masses. How do we make it less painful? This article addresses one of
the obstacles: the need to specify explicit "frame clauses", expressing what
properties are left unchanged by an operation. It is fair enough to ask the
would-be (human) prover to state what each operation changes, and how, but the
(mechanical) prover also requires knowledge of what it does not change. The
process of specifying and verifying these properties is tedious and
error-prone, and must be repeated whenever the software evolves. it is also
hard to justify, since all the information about what the code changes is in
the code itself.
  The AutoFrame tool presented here performs this analysis entirely
automatically. It applies to object-oriented programming, where the issue is
compounded by aliasing: if x is aliased to y, any update to x.a also affects
y.a, even though the updating instruction usually does not even mention y. This
aspect turns out to be the most delicate, and is addressed in AutoFrame by
taking advantage of a companion tool, AutoAlias, which performs sound and
sufficiently precise alias analysis, also in an entirely automatic way.
  Some practical results of AutoFrame so far are: (1) the automatic
reconstruction (in about 25 seconds on an ordinary laptop) of the exact frame
clauses, a total of 169 clauses, for an 8,000-line data structures and
algorithms library which was previously (with the manually written frame
clauses) verified for functional correctness using a mechanical program prover;
and (2) the automatic generation (in less than 4 minutes) of frame conditions
for a 150,000-line graphical and GUI library. The source code of AutoFrame and
these examples are available for download.
