Exercises 06

Type Checking Arrays

This exercise is designed to make you think about certain aspects of Java's type system.

Please hand in your exercises before Wednesday, Oct. 29th, 8.15am.

A Program

The following Java program defines a Cell class, which stores an integer that can only be set once, and defines its subclass ReusableCell, which has additional functionality to reset the value. It then declares and assigns values to arrays of Cell and ReusableCell objects.

class Cell { int x;
boolean init;
 
    void set(int arg) {
	if (init) 
	    throw new RuntimeException("Initialized a cell twice");
	else {
	    x = arg;
	    init = true;
	}
    }
 
    int get() {
	if (init) 
	    return x;
	else 
	    throw new RuntimeException("Called get on uninitialized cell");
    }
}
class ReusableCell extends Cell {
    void reset(int arg) {
	x = arg;
	init = true;
    }
}
class Test {
    public static void main(String[] args) {
	ReusableCell[] rcells;
	Cell[] cells;
 
	rcells = new ReusableCell[2];
	rcells[0] = new ReusableCell();
	rcells[0].reset(42);
 
	cells = rcells;
	cells[1] = new Cell();
	cells[1].set(13);
 
	rcells[1].reset(7);
    }
}

Problem 1 (Warm-Up)

Understand the program above and answer the following:

Do you believe this program should type check using Java compiler? Try and report result of compilation.
If needed, make the smallest possible modification to make the program compiles in Java and report any lines that you needed to modify, if any.
Run the resulting program and explain what happens. Pay attention to line numbers.
Can you suggest any alternative behavior of run-time virtual machine that would result in a different execution of this example?

Problem 2

We next consider type system rules for programs such as the one above, but in a very simple language fragment.

Consider a language that has only 4 built-in types:

Cell
ReusableCell
Cell[]
ReusableCell[]

Assume further that a program in the language is a sequence of local variable declarations, followed by a sequence of 2 kinds of statements:

assignment
method call

The left side of an assignment is either a variable or an array access. The right hand-side of an assignment is

another variable
expression 'new T' where T is one of the 4 types
array access such as 'cells[0]'

Suppose that $\Gamma$ contains the binding of all declared local variables, so that $\Gamma(x)$ gives the declared type of variable $x$ . (In the example above above, $\Gamma(cells) = Cell[]$ .)

In a language without inheritance, we could have the following simple assignment rule

$\begin{equation*} \frac{\Gamma \vdash x : T, e : T} {\Gamma \vdash (x = e) : void} \end{equation*}$

where $T$ denotes arbitrary type. If we had only rule above for assignment, it would not permit code such as

Cell c;
c = new ReusableCell();

which is allowed in Java. We can therefore introduce additional rules, such as

$\begin{equation*} \frac{\Gamma \vdash x : Cell, e : ReusableCell} {\Gamma \vdash (x = e) : void} \end{equation*}$

What should be the complete set of type rules for the assignment statement (x=e) for any left-hand side x and any expression e, in each of the following 3 cases:

to prevent all run-time errors
to obtain the results as in Java
to allow execution of the following program fragment (omitting the last statement in the original program):

	rcells = new ReusableCell[2];
	rcells[0] = new ReusableCell();
	rcells[0].reset(42);
 
	cells = rcells;
	cells[1] = new Cell();
	cells[1].set(13);

Write down the complete set of rules for assignment for each of the three cases above.

Note that we do not wish to assign an array to something that is not an array, or conversely, so certainly programs such as

  Cell c;
  Cell[] cells;
  c = cells;

  Cell c;
  Cell[] cells;
  cells = c

should not be type correct.

If this helps you to be confident about your answer, please feel free to write down and present as part of the answer the rules for the expressions and left-hand sides, but this is not neccessary: we are interested in rules for the assignment statement.