[Prev][Next][Index][Thread]
Re: Subject Reduction in Java -- without joins -- part 2
-
To: types@cs.indiana.edu
-
Subject: Re: Subject Reduction in Java -- without joins -- part 2
-
From: Sophia Drossopoulou <scd@doc.ic.ac.uk>
-
Date: Tue, 23 Jun 1998 19:23:56 +0100
-
Delivery-Date: Tue, 23 Jun 1998 13:26:15 -0500
Further to Don's message, I would like to outline how subject
reduction may be proven for expressions with several different types,
and point out that my earlier suggestion (Saturday)
[on proving type soundness for conditional expressions in Java
by distinguishing between types in Java, the original language, and
types in Java_R, the run-time language], can be simplified
considerably.
1) For Java the type rule for conditionals remains as is, i.e.
b : bool e1:E1 e2:E2
(E1 < E2 and E2=T) or ( E2 < E1 and E1=T)
----------------------------------------------
(b?e1:e2) : T
where < indicates the usual widening (subtype) relation
2) For Java_R the type rule for conditionals is
b : bool e1:E1 e2:E2
E1 < T E2 < T
----------------------------
(b?e1:e2) : T
Thus, in Java_R, conditional expressions may have many types,
therefore, Java_R expressions may have several types.
For instance, in the example that comes later, holds that:
x:X, y:Y |- ( (3>4) ? x : y ) : A
and also,
x:X, y:Y |- ( (3>4) ? x : y ) : D
3) The "OO polymorphism property" holds for Java_R
in the usual form (modulo some quantifiers)
For all \Gamma, T1, ... Tn, T'1, ... T'n, T:
If \Gamma, X1:T1, .. Xn:Tn |- e : T
and each Ti' < Ti,
then, there exists a type T', such that
* \Gamma, X1:T1', .. Xn:Tn' |- e : T'
* T' < T
This property does not say, on the other hand, that
\Gamma, X1:T1', .. Xn:Tn' |- e : T' => T'<T.
For instance, in the example that comes later, holds that:
x:A, y:A |- ( (3>4) ? x : y ) : A
and also,
X < A
Y < A
and also,
x:X, y:Y |- ( (3>4) ? x : y ) : A
but also
x:X, y:Y |- ( (3>4) ? x : y ) : D (notice that NOT D < A )
4) The usual subject reduction can be shown for JavaR, as:
If \Gamma |- e : T, and e non-ground,
then, there exist T', e' such that
1. Case * e rewrites to e'
* \Gamma |- e' : T'
* T' < T
2. Case an exception was raised
5) From this, we prove soundness stating, that execution
of a term t, with |- t : T results in
1. Case a ground value v, with
|- v : T', and
T' < T
2. Case non-termination
3. Case an exception
Notice that in 3) and 4) there may exist further types T''
with |- e' : T'', and NOT ( T''< T). This
does not diminish the soundness result, because ground terms
have unique types.
Sophia
---------------------------------------------------------------------
PS For clarification, here is an example:
interface A { int f(); int g(); }
interface B extends A { }
interface C extends A { }
interface D { int f(); }
class X implements B, D { }
class Y implements D, C { }
A anA; A aB; C aC; D aD; X anX; Y aY;
This is described by the following diagram:
A
/ \
/ \
/ \
/ \
/ \
B D C
\ / \ /
\ / \ /
X Y
Then, the expression has type in Java in JavaR
( (3>4) ? aB : anA ) A A, Object
( (3>4) ? aB : aC ) Error A, Object
( (3>4) ? aB : aD ) Error Object
( (3>4) ? aB : aY ) Error A, Object
( (3>4) ? anX : aY ) Error A, D, Object
( (3>4) ? aB : anA ).f() A int, Error
( (3>4) ? aB : aC ).f() Error int, Error
( (3>4) ? aB : aD ).f() Error Error
( (3>4) ? aB : aY ).f() Error int, Error
( (3>4) ? anX : aY ).f() Error int, int, Error
( (3>4) ? aB : anA ).g() A int, Error
( (3>4) ? aB : aC ).g() Error int, Error
( (3>4) ? aB : aD ).g() Error Error
( (3>4) ? aB : aY ).g() Error int, Error
( (3>4) ? anX : aY ).f() Error int, Error,
--
Dr. Sophia Drossopoulou tel: +44 171 594 8368
http://www-ala.doc.ic.ac.uk/~scd/
Department of Computing fax: +44 171 581 8024
Imperial College of Science, Technology and Medicine
LONDON SW7 2BZ, England email: sd@doc.ic.ac.uk