This file is adapted from books/models/jvm/m5/demo.script. First evaluate the following shell commands. The first will show you a Java definition of a recursive factorial. The second will print the bytecode produced by Sun's javac compiler. % cat % javap -c Demo % java Demo 5 % java Demo 17 Point out the bytecode for fact, which starts on the line public static int fact(int); Save that bytecode in a separate buffer, say, "fact". The third command will run that bytecode on 5 and print 120. The fourth produces a negative answer (32 bit int overflow). Now start up ACL2 and execute: (include-book "models/jvm/m5/jvm-fact-setup" :dir :system) (in-package "M5") (defun demo-fact (n) (let ((sched (fact-sched 0 n))) (list (list 'steps (len sched)) (list 'ans (top (stack (top-frame 0 (run sched (make-state (list (cons 0 (make-thread (push (make-frame 0 nil (push n nil) '((INVOKESTATIC "Demo" "fact" 1)) 'UNLOCKED "Demo") nil) 'SCHEDULED nil))) *demo-heap* *demo-class-table*))))))))) (lookup-method "fact" "Demo" *demo-class-table*) will display the M5 bytecode corresponding to the fact method just shown. Compare it to the bytecode in buffer "fact" produced earlier. Then run (demo-fact 5) to execute the bytecode on 5 and get 120. Now do (demo-fact 17) You get the same answer as when we ran "java Demo 17" before. It is negative because of 32 bit int overflow, i.e., you get the lower order 32 bits of the expected answer in twos-complement. Compare with: (int-fix (! 17)) That is the negative number fact is returning: ``the low order 32 bits of the true factorial''. Now prove it: (defthm fact-is-correct (implies (poised-to-invoke-fact th s n) (equal (run (fact-sched th n) s) (modify th s :pc (+ 3 (pc (top-frame th s))) :stack (push (int-fix (! n)) (pop (stack (top-frame th s))))))) :hints (("Goal" :induct (induction-hint th s n)))) The summary shows rules used in the proof. The theorem above says that if you have an M5 state poised to execute the fact method on n in thread th and if you run it a certain number to steps on thread th, you just modify s by incrementing the pc past the invoke instruction (which is 3 bytes) and popping the n off the stack and pushing the low order 32 bits of the true n!.