The iJVM is a JVM-like machine. A state of the iJVM is a list of
length 2. The first component is a call stack and the second is
a class table.
A class table is a list of class declarations.
A class declaration is a list of length 3 containing a class
name, a list of superclasses, and a list of method definitions.
The class name is a string identifying the class.
The list of superclasses is a list of names of
superclasses, starting with the direct superclass of the class,
then its direct superclass, and so on until the class "Object" is
reached. Recall that the class "Object" is the superclass
of all other classes, as per the JVM specification.
A method definition is a list whose first element is a string
corresponding to the method name, its second argument is a list
of formals, and the rest of the list (the cddr) is a method body.
A call stack is a stack of frames.
A frame is a list of length 4, containing a program counter,
local variables, a local stack, and a method body.
A program counter is a natural number.
The local variables are an alist mapping symbols (the
variable names) to integers (their values).
A local stack is a list (whose car is the top of the
stack) of integers.
A method body is a list of instructions.
The instructions of the iJVM are described here.
What to hand in
Define (run s n) so that it returns the state obtained
by stepping state s n times. To step a state,
we first look at the pc (program counter); say that it has the
value i. We then look at the ith instruction (using 0
indexing) of the method body in the top frame and execute it,
obtaining a new state. Note that run is similar to the
sm function in the Mechanized Formal Reasoning about
Programs and Computing Machines paper by Boyer and Moore.
Use the appropriate functions in the ihs book refered to
in the bit-vector discussion for the arithmetic and logical
Write a pair of functions ijvm-fact-program and
ijvm-fact-clock so that for any natural
n, something of the form
(equal (car (stack (run (ijvm-fact-state n)
is a theorem, where the function stack above returns
the stack of the top frame and fact and ijvm-fact-state are
defined as follows.
(defun fact (n)
(if (zp n)
(* n (fact (1- n)))))
(defun ijvm-fact-state (n)
(push (make-frame 0
(invokestatic "Math" "fact")