Inductive Assertions and Operational Semantics

J Strother Moore
March 28, 2003

Abstract

This paper shows how classic inductive assertions can be used in conjunction with an operational semantics to prove partial correctness properties of programs, without the introduction of a verification condition generator.

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.

Relevant Files

Recertifying

After downloading all of the supporting files above, edit the file 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.