[Prev][Next][Index][Thread]
A paper on an imperative core calculus for Java
The following paper:
MJ: An imperative core calculus for Java and Java with effects
(Tech Report 563, University of Cambridge Computer Laboratory)
by G.M. Bierman, M.J. Parkinson and A.M. Pitts
is now available at:
http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-563.pdf
Comments welcomed!
Abstract:
In order to study rigorously object-oriented languages such as Java or
C#, a common practice is to define lightweight fragments, or calculi,
which are sufficiently small to facilitate formal proofs of key
properties. However many of the current proposals for calculi lack
important language features. In this paper we propose Middleweight
Java, MJ, as a contender for a minimal imperative core calculus for
Java. Whilst compact, MJ models features such as object identity,
field assignment, constructor methods and block structure. We define
the syntax, type system and operational semantics of MJ, and give a
proof of type safety. In order to demonstrate the usefulness of MJ to
reason about operational features, we consider a recent proposal of
Greenhouse and Boyland to extend Java with an effects system. This
effects system is intended to delimit the scope of computational
effects within a Java program. We define an extension of MJ with a
similar effects system and instrument the operational semantics. We
then prove the correctness of the effects system; a question left open
by Greenhouse and Boyland. We also consider the question of effect
inference for our extended calculus, detail an algorithm for inferring
effects information and give a proof of correctness.