LMF - CIn/UFPE
Co-op
Formal Bytecode Generation for a ROOL Virtual Machine
We are concerned with correct
object-oreiented programming language implementations. The design of correct
compilers for procedural languages is already established; now the main challenge is the
development of an approach to deal with object-oriented features. We present an
algebraic approach to design compilation rules for an object-oriented language based on
Java. We define the behavior of the target machine by an interpreter written in the
source language itself. Thus, the compilation task is reduced to one of program
refinement achieved by a series of correctness-preserving transformations which can be
used to generate bytecodes for a sequential subset of a Java Virtual Machine. The
correctness of the compiler follows from the correctness of each algebraic transformation.
Reference
Formal Bytecode Generation for a ROOL Virtual Machine
Adolfo Duran, Augusto Sampaio and Ana Cavalcanti
4th Brazilian Workshop of Formal Methods, 2001.
Revista de Informática Teórica e Aplicada, 7(1): 49-68, 2000.
Click here to retrieve a compressed PostScript file containing
a copy of this paper.