Computing Publications

Publications Home » Towards an Operational Semantics ...

Towards an Operational Semantics and Proof of Type Soundness for Java

Sophia Drossopoulou, Susan Eisenbach

Book Chapter
Formal Syntax and Semantics of Java
Issue 3

We give an operational semantics for a large subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null, arrays and exception throwing and handling. We build a model that is simple and near the programmer's intuition. We distinguish between three languages: Javas is the original language. Javase is an enriched version of Javas containing compile time information necessary for execution. Javar is an extended version of Javase allowing for runtime constructs such as addresses.

We give a type system for Javas, Javase and Javar. The two latter are slight modifications of the former. We prove that well-typed Javas terms retain their type when the corresponding Javase or Javar term is considered. The operational semantics describes the execution of Javar terms for given Javase programs. We prove a subject reduction theorem, which states that execution of Javar preserves types, up to subclasses/subinterfaces

Distributed Software Engineering
Java Semantics
PDF of full publication (414 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.