March 28, 2003

In particular, we show how a formal statement about the operational semantics can be deduced more or less directly from verification conditions. Indeed, we show how the verification conditions can be generated as a side-effect of a ``natural'' proof strategy.

Both iterative and recursive programs are considered. Assertions are attached to the program by defining a predicate on states. This predicate is then ``completed'' to an alleged invariant by the definition of a tail-recursive partial function defined in terms of the state transition function of the operational semantics. If this alleged invariant can be proved to be an invariant under the state transition function, it follows that the assertions are true every time they are encountered in execution and thus that the post-condition is true if reached from a state satisfying the pre-condition. But because of the manner in which the alleged invariant is defined, the verification conditions are sufficient to prove invariance. The fact that the assertions are completed via tail-recursion means that it is unnecessary to prove that the completion process terminates. Indeed, the invariant function may be thought of as a state-based verification condition generator built in a single function definition from the state transition function of the operational semantics.

The method allows standard inductive assertion style proofs to be constructed directly in an operational semantics setting. To demonstrate the technique, a pre-existing model of the Java Virtual Machine is used as the operational semantics. Partial correctness theorems about several simple Java methods are presented. These theorems are contrasted total correctness results proved by defining ``clock functions'' that characterize how many steps are to be executed.

- a short version of the paper for the general audience (172KB postscript) (202K pdf)
- a long version of the paper for the general audience (345KB postscript) (189K pdf)
- a more comprehensive treatment of recursive methods for the ACL2 audience (163KB postscript) (201K pdf)
- some examples in ACL2
- supporting ACL2 scripts. You will need all the
files on this directory if you wish to reproduce the proofs in
`vcg-examples.lisp`

.

`utilities.lisp`

. In it you
will find `include-book`

commands that mention the standard books
`books/arithmetic/top-with-meta`

and
`books/ihs/quotient-remainder-lemmas`

. Change these pathnames to
those for your machine.
Then, while connected to the directory on which you downloaded the files,
fire up ACL2 and execute
`(ld "certify.lsp" :ld-pre-eval-print t)`

.

Recertification takes just a few minutes.