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
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.