Formal JVM specification

[Peter Michael Bertelsen]

Dan Lambright wrote:
> I have not seen a formal desription of Java's bytecode verifier. I have 
> emailed Sun and Princeton's SIP group- no reply.. anyone heard of efferts 
> along these lines?

I've written a report, `Semantics of Java Byte Code', giving a formal
description of the JVM and the bytecode instructions.  The JVM is
modelled as an infinite state machine, and each byte code instruction
is described by a transition rule, describing the state change and the
conditions under which execution succeeds.  The report also lists a
number of errors and ambiguities in Sun's specification of the JVM.

This might be of interest to you, although some aspects of class file
verification are not covered, e.g. checking that the file has the
correct structure.  The report is available at:

  ftp://ftp.dina.kvl.dk/pub/Staff/Peter.Bertelsen/jvm-semantics.ps.gz

Also check out the `Defensive JVM' project at Computational Logic:

  http://www.cli.com/software/djvm/

-Peter Bertelsen