  B.4 Safety (Theorem 2)

Proof:
Let us assume |- ( D ||- P). By Chemical-Solution and Definition, |- ( D ||- P) holds provided
 (Ay|- D :: Ax) y x   #  D Î D (1)

 (Ay|- P) y   #  P Î P  (2)

 A = Èy x   #  D Î D Ax  (3)
We check that no case listed in Definition 1 (Section 6.1) can occur.

##### No free variables.
By definition of type judgments, since (1) hold, every free object name in D, with y x   #  D Î D, should appear as a leaf of the proof tree of Ay|- D :: Ax. This leaf must be of the form Ay+ A' |- x : t. This implies that x belongs to the domain of Ay because x is free in D. Similarly, every class variable in D should belong to the domain of Ay, which actually only contains object names. The proof is similar for free names in P using (2).

##### No runtime failure.
Let y   #  x. l (u) Î P and y' x   #  D Î D (4).
1. (no privacy failure) Let l be a private label f. We prove that y'x is a prefix of y. A derivation of Ay |- x.l (uii Î I) must be:
[Send]
((5))
 ...
 Ay |- x.f : (ti i Î I)
(Ay |- ui : ti)i Î I
 Ay |- x.l (uii Î I)
where (5) is an instance of Private-Message. The premise of (5) requires that x : " X.(l : (tii Î I); B') be in Ay. Therefore, by definition of Ay, variable x must appear in y. Furthermore, by well-formedness of chemical solutions, a name can have a unique prefix. Since y' is already a prefix of x, then y must be of the form y' x y''.

2. (no undeclared label) We show that l Î dl(D). Given (4), the judgment Ay' |- D :: Ax, where Ax = x: " X. r, x: " X.(B | F ), follows by rule Definition applied to (1) with the premises below:
 Ay' |- self(x)  D :: z(r) BW,Ø (6)

 r = B| M (7)

 X = Gen (r, B, Ay') \ ctv(B|W)
Since Ay|- x.l (u) by (2), either r is of the form [l : t; r'] or B is of the form (l : t; B') depending on whether l is public or private. In each case, using (7), l is in dom(B). The conclusion follows by Lemma 7.

3. (no arity mismatch) Let D be of the form [M |> P] where M is itself of the form l(y) & J. We show that y and u have the same arities.

For that purpose, it suffices to show that the type of u and the type of y in A are instances of a same tuple type. A leaf of (6) must be
[Reaction]
(
Message-Pattern
 (yi : t'i Î A')i Î I
 A' |- l (y):: l : (t'ii Î I)
)
 l(y) Î M
 A' |- M :: B ·    ·    ·
 dom(A') = fn(M)      Ay' + x : [r], x : (B | F)+ A' |- P
 Ay' + x : [r], x : (B | F) |- M |> P :: z(r)Bcl(M),Ø
Therefore, the type of y in A' is B(l). By rules Chemical-Solution and Definition, A contains a generalization of x : [r], x : (B | F). Thus, the type of x.l in Ay is a generalization of B(l). The proof tree illustrated in item 1 is required to prove Ay |- x.l (uii Î I). Then, as a consequence of rule (5), the type of u is an instance of the type of x.l in Ay, i.e. of the generalization of the type of y in A'.
##### No class rewriting failure.
Let y   #  P Î P, P = obj x = C init Q in Q', rule Class-Red does not apply to P, i.e. there is no C' such that C |-x® C', and P is not a refinement error. We show that P is not a failure; namely, for every evaluation context E,
1. C ¹ E{c}, and c is free. By (1), dom(A) only contains object names. Therefore, by (2), P cannot contain free class names.
2. Let E {L} = C' or L (the case E {L} = L or C' is similar). We demonstrate that, if A' |- C' or L :: z(r)BW,V then L Í V. By rule Abstract, A' |- L :: z(r)B1Ø,L (8). Let A' |- C' :: z(r)B2W2,V2 (9) and V1' = L \( dom(B2) \ V2(10) and V2' = V2 \( dom(B1) \ L(11). Since there does not exists C'' such that C |-x® C'', the rule Abstract-Cut cannot be applied. This means that L = L \ dl(C') = L \ dom(B2), which implies V1' = L. By (8), (9), (10), (11) and rule Disjunction we obtain A' |- C or L :: z(r)(B1 Å B2)W1 È W2, L È V2' (12).

On the other hand, by (2), a derivation of Ay|- P must contain (P = obj x = C init Q in Q')
[Object]
[Self-Binding]
 Ay+ x : [r],   x.(B | F) |- (C' or L) :: z(r)BW,Ø(13)
 Ay|- self(x)  (C' or L) :: z(r)BW,Ø
r = B | M      X= Gen (r, B, A) ctv(B|W)
Ay+ x : " X. [r], x : " X. (B | F) |- Q      Ay+ x : " X. [r] |- Q'
 A |- obj x = (C' or L) init Q in Q'
To conclude, observe that (12) and (13) do not unify because virtual labels in (12) are not empty.  