Proving Theorems About Java-Like Byte Code - Correct System Design: Recent Insights and Advances - page 153

While both clock expressions and the Lisp functions describing the semantics
of TJVM methods might appear complicated, it is crucial to remember the
compositional nature of specications and proofs. Once the clock expression for
a method has been written and the corresponding specication has been proved,
it is not necessary to think about or reveal the details. For example, one need not
know that (fact-clock 5) is 50, only that (fact-clock n ) is cost of running

fact on .

The use of clocks encourages a focus on terminating computations but does
not preclude consideration of non-terminating computations. By adding a flag
to the TJVM state indicating whether the computation halted normally or \ran
out of time" it is possible to phrase partial correctness results in this framework.
In this setting, typical partial-correctness theorems have the additional hypoth-
esis \provided

n

n

is sucient to guarantee termination." Furthermore, one can
use explicit clocks, as we do, but address oneself to non-terminating computa-
tions and still characterize the state produced at certain points in the innite
computation.
Our toy JVM ignores many aspects of the JVM, as noted earlier, including
the omission of many byte code instructions, the niteness of resources, error
handling, exceptions, and multiple threads. Many of these aspects could be in-
corporated into a formal model. Some, such as the inclusion of additional byte
codes, would not aect the complexity of proofs at all. The others would pre-
serve the basic character of the theorems and proofs described here but, in some
cases, would require the explicit statement of additional hypotheses to insure the
suciency of available resources and the absence of errors. New proof machinery
would have to be created (via the proofs of suitable lemmas) to enable ACL2 to
reason about TJVM computations in which exceptions are thrown or multiple
threads are used.
Our experience, notably that reported in Young's dissertation, [13] and in the
author's work on Piton [11], is that when dealing with resource limitations and
exceptions it is best to produce several layers of abstraction, each formally related
to the next by lemmas, one of which is free of those concepts and corresponds to
our tjvm . That is, we see a model like our TJVM as being a component of a stack
of abstract machines that enables formal discussion of programming language
concepts not included in tjvm .
Cohen's defensive JVM, dJVM, [6] is an example of a machine in such a
hierarchy. Since Cohen's dJVM deals realistically with a signicant fragment of
the actual JVM, we cannot relate it to our TJVM. But we can explain the basic
concept of a \defensive machine" by imagining a \defensive TJVM."
Consider the behavior of our TJVM on the add instruction: the top two items
on the operand stack are added together. What if they are non-numeric? Our
TJVM model answers this question by appealing simply to the untyped ACL2
logic: add uses the total ACL2 function + to combine the two items. This is
simple and allows proofs of byte code program properties. But we probably do
not intend to implement the TJVM fully, i.e., we probably do not intend to mimic
the model's behavior on non-numeric input. To address this we dene another