CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

iJVM Specification

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.

What to hand in

  1. 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 operations.
  2. 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)
    			(ijvm-fact-clock n))))
           (fact 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)
          1
        (* n (fact (1- n)))))
    
    (defun ijvm-fact-state (n)
      (make-state
       (push (make-frame 0
                         nil
                         nil
                         `((bipush ,n)
                           (invokestatic "Math" "fact")
                           (halt)))
             nil)
       (list *math-class*)))
    
    (defconst *math-class*
      `("Math"
        ("Object")
        (("fact" (N)
          ,@(ijvm-fact-program)))))