|
|
|---|
|
|
|
|---|
J S. Moore, “Proving
Theorems about Java-like Byte Code,” in E.-R. Olderog and
B. Steffen, editors, Correct System Design -- Recent Insights and
Advances, LNCS 1710, pp. 139-162, 1999.
Relevance: M2: a JVM model similar to M1 but with
method invocation (i.e., subroutine call)
Recall that in operational-semantics-1__simple-example we described a simple machine akin to the JVM but providing only a few stack-based arithmetic instructions and conditional and unconditional jump instructions. In this paper a similar machine is formalized which provides method invocation and return for both static and virtual methods, and simple class-like instance objects with inheritance. In the paper this machine is called the “toy JVM” or “tjvm.” But if we place it in the evolving sequence of approximations to the JVM it should be named “M2.”
The ACL2 scripts providing the definition and theorems of the
paper (but now using the name