Modern Semantics of Object-Oriented Languages

Presented: Viera Proulx
Transcribed: Therapon Skotiniotis

The talk concentrated on 3 sets of papers all dealing with semantics for modern Object-Oriented (OO) languages, concentrating on Java.

The first group of papers from Drossopoulou, Eisenbanch and Khurshid concentrate on proving Java's type system sound. The question was raised "Why do we need to prove, a type system, sound? What's the point?". After a discussion the conclusion was:

  1. If you get an error then it is a well defined error
  2. Allows the developer to limit his search for an error into a small subset of the code
  3. A meaning to a stream of bits.
The papers use a kernel of Java, where all programs terminate to either a value of compatible type or with an exception and all programs are made up of a collection of class definitions. The papers attempt to cover as big of a subset of Java as possible and model inheritance, membership, shadowing, interfaces, types, dynamic method binding, arrays, object creations and exceptions.

Environments are provided with the following definition:
Env ::= stdEnv | Env; Decl
where stdEnv includes what comes with the standard Java Library. Environments are used to store information about class definitions, field definitions, type, arguments and their types, method types etc. In order to make type information readily available a language two languages are defined.

Java ⊃ Javas → Javase
↓ ↓
Type = Type

Where Javas is the Kernel language and Javas is annotated (through a rewrite step →) extra type information e.g., class where the field is defined, class where a method is defined. A variable can hold an instance of a class or a subtype of that class.

Question: What is the meaning of "type", because you refer to it both at compile and runtime?
Answer: Type is compile time, at runtime this becomes a tag

The rules provided are the typical ones, but there is an addition for widening between types one of the rules states that I can substitute an object of type τ with one of type τ' is the latter is a subtype of the former (τ ⊆ τ'):

Γ |- τ ⊆ τ'
Γ |- τ ≤wdn τ'

In a well-formed environment of Javase subclassing defines a partial order for classes (⊆) and interfaces (≤). The widening rule is partial order. The widening rule extends to deal with method overrides, this is based according to the return type of the method i.e.

τ ≤wdn τ'
↓ ↓
m m'
m ≤wdn m'

Javase has a richer set of type rules (e.g., memory addresses), first fit (the first class for the hierarchy tree that fits), object creation, assignment etc. Operational semantics for Javase is defined as a ternary relationship, mapping configurations and programs to configurations. A configuration is a tuple of Javase terms and states or just state.

Config ::= ⟨ Javase term, state ⟩ ∪ state

Where state is a mapping from identifiers to primitive values or references.

Subject reduction and soundness theorems state that a well-typed program in this subset of Java evaluates to a ground term of the type that can be widened to the type of the original program, or it raises an exception and the state remains consistent with the environment.

The second group of paper consists of a paper by Igarashi, Pierce and Wadler, describing a core subset of Java (Featherweight Java) to which they provide semantics and an extension to handle generics in Java. Unlike the previous group of papers the goal is to define a small core of the language with which most of the language features can be studied. The model defines mutually recursive class definitions, subtypes, casting etc. The goal, well-typed programs do note get stuck.

Question: What to you mean not stuck?
Answer: A program returns a value or an exception.

There are 3 ways to get stuck

  1. access a field that is not defined in a type
  2. call a method not defined by the target type
  3. cast an object to a type that is not a subtype of
1 and 2 never happen on well-typed programs. The paper defines 3 types of casting: Stupid casts eliminate themselves and make proofs work out with greater ease than Classic Java (next group of papers). Operational semantics is defined in terms of reduction rules for field access, method invocation, casting and congruence that can be applied in a context free manner. Subject reduction theorem states:

if Γ |- e ∈ c and e → e' then Γ |- e' ∈ c' for some c' <: c

The progress theorem states that if a well-typed program has a field access or a method invocation then this field or method is well-defined. This leads to the soundness theorem which states that an expression e of the type c in an environment Γ evaluates to e' with e' being in normal form then ' is either a value or it contains an expression with a stupid cast inside it.

The last group of paper by Flatt, Krishnamurthi and Felleisen (Classic Java) define again a core for the Java language. In one of their papers the core language is used to add mixins to Java. The system is very much similar to Featherweight Java with the addition of assignment. The paper defines elaboration rules that translate expression into annotated expressions that include needed type information. Semantics are given as a contextual rewrite system on pairs of expressions and stores.

Matthias summarized the work by the three groups as:

Drossopoulou et. al. 96,
Natural semantics approach, avoiding the trap of polymorphism (Tofte). The reduction semantics proof is big (and buggy).
Flatt et. al. 97
Context sensitive semantics, provide semantic for Java and extend the language to deal with mixins. The language can be thought of as λ-s. One of the cases in the proofs was wrong. The technical report fixed the bug.
Igarashi et. al. 00
Context-free reduction semantics. The language can be though of as λ + records. The language is trivial.
NOTE Flatt et. al. and Igarashi et. al. did not prove soundness of Java, but extended the language to deal with mixins (the former) and generics (the latter). Drossopoulou et. al. prove type soundness for Java.