Previous Up
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(xD :: 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.



Previous Up