3.3 Type Preservation
3.3.4 Type Preservation
We also know thatµ=readtandB0=B1. SinceΓ00=sideEffect(readt,Γ) = Γ by the definition of sideEffect (3.12) we are going to prove that Γ ` B0.Γ0.
Applying the Inversion Lemma (Lemma 3.9) toΓ `B if(e)B1else B2. Γ0 we know that it can only be typed by rule T-If-Then-Else:
(T-If-Then-Else) Γ`e:boolΓ` Γ`BB1.Γ0 Γ`BB2.Γ0
Bif(e)B1else B2.Γ0
The thesis follows by premiseΓ `B B1 . Γ0. Case B-If-Else The proof is similar to case B-If-Then.
Case B-Par
In this case, we knowB=B1 |B2 for some behavioursB1andB2:
(B-Par) B1
−→µ B01 B1 |B2−→µ B01|B2
We also knowB0 =B01|B2.
Applying the Inversion Lemma (Lemma 3.9) on Γ `B B1 | B2 . Γ0 we know that it can only be typed by rule T-Par where Γ = Γ1,Γ2 and Γ0= Γ01]Γ02:
(T-Par) Γ1`BB1.Γ01 ΓΓ2`BB2.Γ02 Roots(Γ01)∩Roots(Γ02)=∅
1,Γ2`BB1|B2.Γ01]Γ02 (3.16) By applying the induction hypothesis to the premise of B-Par,B1
−→µ B10, and premise,Γ1 `B B1 .Γ01, of T-Par we getΓ001 `B B01. Γ01whereΓ001= sideEffect(µ,Γ1). Since it is not possible to remove variables from an envi-ronment by the form of the type system andSideEffectwe know byΓ001 `B
B01 . Γ01from the induction hypothesis and byRoots(Γ01)∩Roots(Γ02) =∅ from 3.16 thatRoots(Γ001)∩Roots(Γ2) =∅. Since it is not possible to alter operations by the form of the type system andSideEffect we also know
Γ001∩Γ2=∅ (3.17)
From the conclusion of 3.16 we knowΓ01]Γ02. Since we knowΓ001∩Γ2=∅ andΓ01]Γ02 then withΓ001 `B B10 . Γ01 from the induction hypothesis and Γ2 `B B2 . Γ02 andRoots(Γ01)∩Roots(Γ02) =∅ from T-Par onB, we can now apply T-Par onB0:
(T-Par) Γ001`BB10.Γ01 ΓΓ002`BB2.Γ02 Roots(Γ01)∩Roots(Γ02)=∅
1,Γ2`BB10 |B2.Γ01]Γ02
In order for the thesis to follow from the conclusion of this rule, we must have Γ001 ]Γ2 = sideEffect(µ,Γ). In order to prove that, we first prove Roots(µ)⊆Keys(sideEffect(µ,Γ)), whereKeys(Γk)denotes the keys inΓk for an environmentΓk.
Let Roots(e) be the set of roots of variables in an expression e, and let Roots(µ) be the set of roots of variables in a label µ including roots of variables from any expressions inµ.
Let a well-typed behaviourB typed under an environmentΓtake a tran-sition labelledµ. Let the transition updateΓ to Γ00. The set of variable roots inµis a subset of the set of variable roots inΓ00.
Lemma 3.14
If Γ `B B . Γ0 andB −→µ B0
then Roots(µ)⊆Keys(sideEffect(µ,Γ))
Proof.
The proof is a case analysis over the labels.
Caseµ=x =e
From the case we knowRoots(µ) = r(x)∪Roots(e). From the form of SideEffect we know that in order for SideEffect to return, there exists two possibilities for a transition taken with this label:
Subcase SideEffect(x =e,Γ) = Γ
From the for of sideEffect we knowΓ ` e: Te andx:Tx ∈Γ.
By Γ ` e : Te we know Roots(e) ⊆ Keys(sideEffect(x =e,Γ)).
By x : Tx ∈ Γ we know r(x) ∈ Γ from the form of sideEf-fect. By r(x) ∈Γ and SideEffect(x =e,Γ) = Γ we knowr(x)∈ Keys(sideEffect(x =e,Γ)).
Subcase SideEffect(x =e,Γ) =upd(Γ, x, bt(Te))
From the for ofsideEffect we knowΓ ` e:Te. ByΓ ` e:Tewe know Roots(e)⊆Keys(sideEffect(x =e,Γ)). By the form of upd we knowr(x)∈Keys(sideEffect(x =e,Γ)).
Caseµ= (r,o@l)?x
The proof is similar to the proof for caseµ=x =e.
Caseµ=r:o(x)
The proof is similar to the proof for caseµ=x =e.
Case µ=readt
From the case we knowRoots(µ) =∅. The thesis follows immediately.
Case µ=νro@l(e)
From the case we knowRoots(µ) =Roots(e)andsideEffect(νro@l(e),Γ) = Γ. From the for ofsideEffect we knowΓ ` e:Te. ByΓ ` e:Teand
sideEffect(νro@l(e),Γ) = Γwe knowRoots(e)⊆Keys(sideEffect(νro@l(e),Γ)).
Case µ= (r,o)!x
From the case we knowRoots(µ) =r(x)andsideEffect((r,o)!x,Γ) = Γ. From the for ofsideEffect we know x: Tx ∈ Γ. By x: Tx ∈ Γ we knowr(x) :Tx∈Γfrom the form ofsideEffect. Fromr(x) :Tx∈Γ
andsideEffect(νro@l(e),Γ) = Γwe knowr(x)∈Keys(sideEffect(νro@l(e),Γ)).
By B1
−→µ B10 from the case, Γ1 `B B1 . Γ01 from 3.16 and Lemma 3.14 we know Roots(µ) ⊆ Keys(SideEffect(µ,Γ1)). Since it is not pos-sible to remove variables from an environment by the form of the type system and SideEffect we know by Roots(µ) ⊆ SideEffect(µ,Γ1) and by SideEffect(µ,Γ1) `B B10.Γ01from the induction hypothesis and byRoots(Γ01)∩
Roots(Γ02) =∅ from 3.16 that Roots(µ)∩Γ02 =∅. Since it is not possible to remove variables from an environment by the form of the type system andSideEffectwe know byRoots(µ)∩Γ02=∅and byΓ2 `B B2.Γ02from 3.16 that
Roots(µ)∩Γ2=∅ (3.18)
If two environmentsΓ1andΓ2are disjoint and if the effect of executing a label µin the contextΓ1, updatesΓ1 toΓ001 and if the set of roots of the variables in µare disjoint to Γ2 then the disjoint union of Γ2 to Γ1 does not influence the updates performed by executingµ.
Lemma 3.15
If SideEffect(µ,Γ1) = Γ001 andΓ1∩Γ2=∅
and Roots(µ)∩Γ2=∅
then SideEffect(µ,(Γ1]Γ2)) =SideEffect(µ,Γ1)]Γ2
Proof.
The proof is a case analysis over the labels.
Case µ=x =e
Since we know Roots(x =e)∩Γ2 = ∅ we know that x /∈ Γ2 and that Roots(e)∩Γ2 = ∅. We therefore know that since we have SideEffect(x =e,Γ1) = Γ01 then union Γ2 to the input, does not in-fluence the branch chosen inSideEffect.
The rest of the cases are similar.
Recall we in 3.17 havesideEffect(µ,Γ1)∩Γ2=∅and thatΓ = Γ1,Γ2. The thesis follows bysideEffect(µ,Γ1) = Γ001 from the induction hypothesis and byΓ1∩Γ2, 3.18,sideEffect(µ,Γ1)∩Γ2=∅ and Lemma 3.15.
Case B-Seq
In this case, we knowB=B1;B2 for some behavioursB1and B2: (B-Seq) B1
−→µ B01 B1;B2
−→µ B01;B2
We also knowB0 =B10;B2. Applying the Inversion Lemma (Lemma 3.9) toΓ `B B1;B2 . Γ0 we know that it can only be typed by rule T-Seq:
(T-Seq) Γ`BB1Γ.Γ`000 Γ000`BB2.Γ0
BB1;B2.Γ0
By applying the induction hypothesis on the premiseB1
−→µ B10 of B-Seq and premise Γ `B B1 . Γ000 of T-Seq, we get Γ001 `B B10 . Γ000 where Γ001 =sideEffect(µ,Γ).
We can now apply T-Seq on B0 with the two premises, Γ001 `B B10 . Γ000 from the induction hypothesis andΓ000 `B B2. Γ0 from T-seq used onB:
(T-Seq) Γ
00
1`BB01.Γ000 Γ000`BB2.Γ0 Γ001`BB10;B2.Γ0
In order for the thesis to follow from the conclusion of T-Seq applied on B0 we must have that Γ001 = Γ00. Since Γ001 = sideEffect(µ,Γ) and Γ00=sideEffect(µ,Γ) thenΓ001 = Γ00.
Case B-Iteration
In this case, we know B = while(e){B1} for an expression e and a behaviourB1:
(B-Iteration) e(t)=true
while(e){B1}−−−−→readt B1;while(e){B1}
We also know that µ=read t andB0 =B1;while(e){B1}. Since Γ00= sideEffect(readt,Γ) = Γby the definition ofsideEffect(3.12) we are going to prove thatΓ `B B0 . Γ0.
Applying the Inversion Lemma (Lemma 3.9) toΓ `B while(e){B1}.Γ0 we know that it can only be typed by rule T-While:
(T-While) ΓΓ``e:bool Γ`BB1.Γ
Bwhile(e){B1}.Γ
Notice that B is only typable for cases where Γ0 = Γ. Therefore we are going to proveΓ `B B0 .Γ. By premiseΓ `B B1.Γand the conclusion Γ `B while(e){B1} . Γ in T-While applied on B we can now apply T-Seq on B0:
(T-Seq) Γ`BBΓ1`.Γ Γ`Bwhile(e){B1}.Γ
BB1;while(e){B1}.Γ
The thesis follows from the conclusion of T-Seq applied on B0. Case B-No-Iteration
If the last rule in the derivation sequence is B-No-Iteration, then from the form of this rule, we see that B=while(e){B1}for an expressioneand a behaviourB1:
(B-No-Iteration) e(t)=f alse while(e){B1}−−−−→readt 0
We also know that µ =read t and B0 = 0;while(e){B1}. Since Γ00 = sideEffect(readt,Γ) = Γby the definition ofsideEffect(3.12) we are going to prove thatΓ `B B0 . Γ0.
Applying the Inversion Lemma (Lemma 3.9) toΓ `B while(e){B1}.Γ0 we know that it can only be typed by rule T-While:
(T-While) ΓΓ``e:bool Γ`BB1.Γ
Bwhile(e){B1}.Γ
From the conclusion of this rule we have that Γ0 = Γ. Therefore we are going to prove Γ `B B0 . Γ. The thesis follows from applying T-Nil on B0 =0.
Case B-Assign
In this case, we knowB=x =efor an expressioneand a variablex:
(B-Assign) x =e −−−→x =e 0
We also know thatµ=x =eandB0 =0.
Applying the Inversion Lemma (lemma 3.9) onΓ `B x =e . Γ0 we know that it can be typed by two different rules. We therefore consider each case:
Subcase T-Assign-New
IfΓ `B x =e .Γ0 is typed using T-Assign-New, then we see from the form of this rule thatΓ0=upd(Γ, x, bt(Te)):
(T-Assign-New) Γ` Γ`e:Te x /∈Γ
Bx =e .upd(Γ,x,bt(Te))
By premise Γ ` e : Te and x /∈ Γ from T-Assign-New applied on B and by label x =e we have that Γ00 = sideEffect(x =e,Γ) = upd(Γ, x, bt(Te))by the definition ofsideEffect (3.12). Therefore we are going to prove thatupd(Γ, x, bt(Te)) `B P0 . upd(Γ, x, bt(Te)).
The thesis follows from applying T-Nil onB0 =0.
Subcase T-Assign-Exists
IfΓ `B x =e .Γ0 is typed using T-Assign-Exists, then we see from the form of this rule thatΓ0 = Γ:
(T-Assign-Exists) Γ`e:Te x:TΓ`x∈Γ bt(Te)=bt(Tx)
Bx =e .Γ
We are therefore going to prove that Γ00 `B B0 . Γ. By premise Γ ` e : Te, x: Tx ∈ Γ and bt(Te) = bt(Tx) from T-Assign-Exists applied onB and by labelx =ewe have thatsideEffect(x =e,Γ) = Γ by the definition ofsideEffect(3.12). Therefore we are going to prove Γ `B B0 . Γ. The thesis follows from applying T-Nil onB0=0.
Case B-Notification
In this case, we knowB =o@l(e)for an expressione and an operationo at a locationl:
(B-Notification) o@l(e) −−−−−−→νro@l(e) 0
We also know that µ =νro@l(e)and B0 =0. Applying the Inversion Lemma (Lemma 3.9) to Γ `B o@l(e) . Γ0 we know that it can only be typed by rule T-Notification:
(T-Notification) o@l:<To>∈ΓΓ` Γ`e:Te Te≤To
Bo@l(e).Γ
From the conclusion of this rule we know that Γ0 = Γ. Therefore we are going to prove Γ00 `B B0 . Γ. By the premises of this rule together with labelνro@l(e)we have that Γ00 =sideEffect(νro@l(e),Γ) = Γ by the definition of sideEffect (3.12). Therefore we are going to prove that Γ `B B0 . Γ. The thesis follows from applying T-Nil onB0=0.
Case B-SolResp
If the last rule in the derivation sequence is B-SolResp, then from the form of this rule, we see thatB=o@l(e)(x)for an expressione, a variablex,an operationoat a locationl:
(B-SolResp) o@l(e)(x) −−−−−−→νro@l(e) Wait(r,o@l,x)
We also know thatµ=νro@l(e)andB0 =Wait(r,o@l,x). Applying the Inversion Lemma (Lemma 3.9) to Γ `B o@l(e)(x) . Γ0 we know that it can be typed by two rules. We therefore consider both cases:
Subcase T-SolResp-New
If Γ `B o@l(e)(x) . Γ0 is typed using T-SolicitResponse-New then we see from the form of this rule thatΓ0=upd(Γ, x, Ti):
(T-SolResp-New) o@l:<To,TΓi`>∈Γ Γ`e:Te Te≤To x /∈Γ
Bo@l(e)(x).upd(Γ,x,Ti)
Therefore we are going to proveΓ00 `B B0 . upd(Γ, x, Ti).
By premise o@l : <To, Ti> ∈ Γ,Γ ` e:Te and Te≤To of this rule and by labelνro@l(e)we have thatΓ00=sideEffect(νro@l(e),Γ) = Γ by the definition of sideEffect (3.12). Therefore we are going to prove thatΓ `B B0 .upd(Γ, x, Ti). The thesis follows from applying rule T-Wait-New onΓ `B Wait(r,o@l,x) . upd(Γ, x, Ti)by premise o@l : <To, Ti> ∈ Γ and x /∈ Γ from T-SolResp-New applied on Γ `B o@l(e)(x). Γ0:
(T-Wait-New) Γ`o@l:<To,Ti>∈Γ x /∈Γ
BWait(r,o@l,x).upd(Γ,x,Ti)
Subcase T-SolicitResponse-Exists
IfΓ `B o@l(e)(x).Γ0is typed using T-SolicitResponse-Exists then we see from the form of this rule thatΓ0= Γ:
(T-SolResp-Exists) o@l:<To,Ti>∈Γ Γ`Γe:T` e Te≤To x:Tx∈Γ Ti≤Tx
Bo@l(e)(x).Γ
Therefore we are going to proveΓ00 `B B0 . Γ.
By premiseo@l:<To, Ti> ∈ Γ,Γ ` e:TeandTe≤Toof this rule and by label νro@l(e)we have that Γ00 =sideEffect(νro@l(e),Γ) = Γ by the definition ofsideEffect(3.12). Therefore we are going to prove that Γ `B B0 . Γ. The thesis follows from applying rule T-Wait-Exists on Γ `B Wait(r,o@l,x) . Γ by premise o@l : <To, Ti> ∈ Γ, x : Tx ∈ Γ and Ti ≤ Tx from T-SolResp-Exists applied on Γ `B o@l(e)(x) . Γ0:
(T-Wait-Exists)o@l:<To,TΓi`>∈Γ x:Tx∈Γ Ti≤Tx
BWait(r,o@l,x).Γ
Case B-OneWay
If the last rule in the derivation sequence is B-OneWay, then from the form of this rule, we see thatB=o(x) for an operation o and a variable x:
(B-OneWay) o(x) −−−−→r:o(x) 0 We also know thatµ=r:o(x) andB0=0.
Applying the Inversion Lemma (Lemma 3.9) toΓ `B o(x) . Γ0 we know that it can be typed by two different rules. We therefore consider both cases:
Subcase T-OneWay-New
IfΓ `B o(x) . Γ0 is typed using T-OneWay-New, then we see from the form of this rule thatΓ0 =upd(Γ, x, Ti):
(T-OneWay-New) Γ`o:<Ti>∈Γ x /∈Γ
Bo(x).upd(Γ,x,Ti)
Therefore we are going to proveΓ00 `B B0 . upd(Γ, x, Ti).
By premisex /∈ Γ and o:<Ti> ∈ Γ in T-OneWay-New applied on B and by labelr:o(x)we have that Γ00=sideEffect(r:o(x),Γ) = upd(Γ, x, Ti)by the definition ofsideEffect (3.12). Therefore we are going to prove thatupd(Γ, x, Ti) `B B0 . upd(Γ, x, Ti). The thesis follows from applying T-Nil onB0=0.
Subcase T-OneWay-Exists
IfΓ `B o(x).Γ0is typed using T-OneWay-Exists, then we see from the form of this rule thatΓ0 = Γ:
(T-OneWay-Exists) o:<Ti>∈ΓΓ`x:Tx∈Γ Ti≤Tx
Bo(x).Γ
Therefore we are going to proveΓ00 `B B0 . Γ. By the premises of T-OneWayExists applied onB and by label r:o(x) we know that Γ00=sideEffect(r:o(x),Γ) = Γby the definition ofsideEffect(3.12).
Therefore we are going to proveΓ `B B0.Γ. The thesis follows from applying T-Nil onB0=0.
Case B-ReqResp
If the last rule in the derivation sequence is B-ReqResp, then from the form of this rule, we see that B =o(x)(x’) {B1} for an operation o, a behaviourB1 and two variablesxandx0:
(B-ReqResp) o(x)(x’) {B1} −−−−→r:o(x) Exec(r,o,x’, B1)
We also know that µ = r : o(x) and B0 =Exec(r,o,x’, B1). Applying the Inversion Lemma (Lemma 3.9) toΓ `B o(x)(x’) {B1}.Γ0we know that it can be typed by two different rules. We therefore consider each case:
Subcase T-ReqResp-New
IfΓ `B o(x)(x’) {B1}. Γ0 is typed using T-ReqResp-New then we see from the form of this rule thatΓ0= Γ000:
(T-ReqResp-New)o:<Ti,To>∈Γ x /∈Γ upd(Γ,x,TΓ` i)`BB1.Γ000 x0:Tx0∈Γ000 Tx0≤To
Bo(x)(x’) {B1}.Γ000
Therefore we are going to prove Γ00 `B B0 . Γ000. By premise o : <Ti, To> ∈ Γ and x /∈ Γ in T-ReqResp-New applied on Γ `B
o(x)(x’) {B1}.Γ0and by labelr:o(x)we have thatΓ00=sideEffect(r: o(x),Γ) =upd(Γ, x, Ti)by the definition ofsideEffect(3.12). There-fore we are going to proveupd(Γ, x, Ti) `B B0 . Γ000.
Since sideEffect does not change operations we have by premise o:
<Ti, To> ∈ Γfrom T-ReqResp-New applied onΓ `B o(x)(x’) {B1}. Γ0 that o:<Ti, To> ∈ Γ00. The thesis follows from applying rule T-Exec onupd(Γ, x, Ti) `B Exec(r,o,x’, B1).Γ000byo:<Ti, To> ∈ Γ00 and premise upd(Γ, x, Ti) `B B1 . Γ000,x0 :Tx0 ∈Γ000 andTx0)≤To from T-ReqResp-New applied onΓ `B o(x)(x’) {B1} . Γ000:
(T-Exec) o:<Ti,To>∈Γ00Γ00Γ`00B`BExec(r,o,x’,BB1.Γ000 1x)0.Γ:Tx0000∈Γ000 Tx0≤To
Subcase T-ReqResp-Exists
If Γ `B o(x)(x’) {B1} . Γ0 is typed using T-ReqResp-Exists then we see from the form of this rule thatΓ0= Γ000:
(T-ReqResp-Exists) o:<Ti,To>∈Γ x:Tx∈Γ Ti≤Tx Γ`BB1.Γ
000 x0:Tx0∈Γ000 Tx0≤To Γ`Bo(x)(x’) {B1}.Γ000
Therefore we are going to proveΓ00 `B Exec(r,o,x’, B1). Γ000. By premiseo:<Ti, To> ∈ Γ,x:Tx ∈ ΓandTi≤Txof this rule and by label r: o(x) we have that Γ00 =sideEffect(r :o(x),Γ) = Γ by the definition of sideEffect (3.12). Therefore we are going to prove Γ `B Exec(r,o,x’, B1) . Γ000. The thesis follows from applying rule T-Exec onΓ `B Exec(r,o,x’, B1).Γ000by premiseo:<Ti, To> ∈ Γ, Γ `B B1 . Γ000, x0 :Tx0 ∈Γ000 and Tx0 ≤To from T-ReqResp-Exists applied onΓ `B o(x)(x’) {B1} . Γ0:
(T-Exec) o:<Ti,To>∈Γ ΓΓ``BB1.Γ000 x0:Tx0∈Γ000 Tx0≤To
BExec(r,o,x’,B1).Γ000
Case B-Exec
In this case, we knowB =Exec(r,o,x, B1)for a channelr, an operation o, a behaviourB1and a variablex:
(B-Exec) B1
−→µ B01
Exec(r,o,x,B1)−→µ Exec(r,o,x,B10)
We also know thatB0 =Exec(r,o,x, B01). Applying the Inversion Lemma (Lemma 3.9) to Γ `B Exec(r,o,x, B1) . Γ0 we know that it can only be typed by T-Exec:
(T-Exec) o:<Ti,To>∈ΓΓΓ`` BB1.Γ000 x:Nx∈Γ000 Tx≤To
BExec(r,o,x,B1).Γ000
From the conclusion of this rule we have thatΓ0 = Γ000. Therefore we are going to proveΓ00 `B Exec(r,o,x, B01) . Γ000.
By applying the induction hypothesis on premise B1
−→µ B10 from B-Exec and on premise Γ `B B1 . Γ000 from T-Exec applied on Γ `B
Exec(r,o,x, B1).Γ000, we getΓ001 `B B10 .Γ000whereΓ001=sideEffect(µ,Γ).
From B-Exec we know that the label for the premise and for the conclusion is the same. We therefore haveΓ00= Γ001.
SincesideEffectdoes not change operations we have by premiseo:<Ti, To> ∈ Γfrom T-Exec applied onΓ `B Exec(r,o,x, B1). Γ000 thato:<Ti, To> ∈ Γ00. The thesis follows from applying T-Exec onΓ00 `B Exec(r,o,x, B10). Γ000 by o : <Ti, To> ∈ Γ00, Γ00 `B B10 . Γ000 from the induction hypoth-esis and premise x : Nx ∈ Γ000 and Tx ≤ To from T-Exec applied on Γ `B Exec(r,o,x, B1) . Γ000.
Case B-End-Exec
If the last rule in the derivation sequence is B-End-Exec, then from the form of this rule, we see that B = Exec(r,o,x,0) for a channel r, an operationoand a variablex:
(B-End-Exec) Exec(r,o,x,0) −−−−−→(r,o)!x 0
We also know thatµ= (r,o)!xand thatB0=0. Applying the Inversion Lemma (Lemma 3.9) to Γ `B Exec(r,o,x,0) . Γ0 we know that it can only be typed by T-Exec:
(T-Exec) o:<Ti,To>∈ΓΓΓ``B0.Γ000 x:Tx∈Γ000 Tx≤To
BExec(r,o,x,0).Γ000
By applying T-Nil on premiseΓ `B 0.Γ000from this rule we knowΓ000= Γ.
Therefore we are going to proveΓ00 `B 0.Γ. By premiseo:<Ti, To> ∈ Γ, x : Tx ∈Γ and Tx ≤ To of T-Exec applied on Γ `B Exec(r,o,x,0) . Γ and by label (r,o)!xwe have thatΓ00=sideEffect((r,o)!x,Γ) = Γby the definition ofsideEffect(3.12). Therefore we are going to proveΓ `B 0.Γ.
The thesis follows from applying rule T-Nil onΓ `B 0. Γ.
Case B-Wait
In this case, we knowB =Wait(r,o@l,x)for a channelr, a variablexand an operationoat a locationl:
(B-Wait)Wait(r,o@l,x) −−−−−−→(r,o@l)?x 0
We also know that µ = (r,o@l)?x and B0 = 0. Applying the Inversion Lemma (Lemma 3.9) to Γ `B Wait(r,o@l,x) . Γ0 we know that it can be typed by two rules. We therefore consider both cases:
Subcase T-Wait-New
If Γ `B Wait(r,o@l,x) . Γ0 is typed using T-Wait-New then we see from the form of this rule thatΓ0 =upd(Γ, x, Ti):
(T-Wait-New)Γ`o@l:<To,Ti>∈Γ x /∈Γ
BWait(r,o@l,x).upd(Γ,x,Ti)
Therefore we are going to proveΓ00 `B B0 . upd(Γ, x, Ti).
By premise o@l :<To, Ti> ∈ Γ and x /∈ Γ of this rule and by label (r,o@l)?xwe have that Γ00=sideEffect((r,o@l)?x,Γ) =upd(Γ, x, Ti) by the definition ofsideEffect(3.12). Therefore we are going to prove that upd(Γ, x, Ti) `B B0 . upd(Γ, x, Ti). The thesis follows from applying rule T-Nil onupd(Γ, x, Ti) `B 0. upd(Γ, x, Ti).
Subcase T-Wait-Exists
IfΓ `B Wait(r,o@l,x).Γ0is typed using T-Wait-Exists then we see from the form of this rule thatΓ0 = Γ:
(T-Wait-Exists) o@l:<To,TΓ`i>∈Γ x:Tx∈Γ Ti≤Tx
BWait(r,o@l,x).Γ
Therefore we are going to proveΓ00 `B B0 . Γ.
By premise o@l :<To, Ti> ∈ Γ,x:Tx ∈ Γ andTi ≤Tx of this rule and by label(r,o@l)?xwe have thatΓ00=sideEffect((r,o@l)?x,Γ) = Γ by the definition ofsideEffect(3.12). Therefore we are going to prove that Γ `B B0 . Γ. The thesis follows from applying rule T-Nil on Γ `B 0 . Γ.
Case B-Choice
In this case, we knowB=P
i∈J[ηi]{Bi}for a sum of behavioursηi and Bi overi:
(B-Choice) j∈J ηj
−→µ Qj P
i∈J[ηi]{Bi}−→µ Qj;Bj
We also know thatB0=Qj;Bj. Applying the Inversion Lemma (Lemma 3.9) toΓ `B P
i∈J[ηi]{Bi} . Γ0 we know that it can only be typed by rule T-Choice:
(T-Choice) ∀j∈J .Γ`Bηj;Bj.Γ
0 Γ`BP
i∈J[ηi]{Bi}.Γ0
By applying the Inversion Lemma (Lemma 3.9) to premiseΓ `B ηj;Bj . Γ0 from this rule we know that it is only typable by T-Seq:
(T-Seq) Γ`Bηj.Γ
000 Γ000`BBj.Γ0
Γ`Bηj;Bj.Γ0 (3.19)
By applying the induction hypothesis on premise Γ `B ηj . Γ000 from 3.19 and premise ηj
−→µ Qj from B-Choice we know Γ0000 `B Qj . Γ000 whereΓ0000=sideEffect(µ,Γ) by the definition ofsideEffect (3.12). Since the premise and the conclusion of B-Choice shares the same label we have Γ00= Γ0000.
The thesis follows from applying T-Seq onΓ00 `B Qj;Bj . Γ0 byΓ00 `B
Qj .Γ000from the induction hypothesis and premiseΓ000 `B Bj . Γ0 from 3.19.
Case B-Struct
From the form of this rule we know thatB =B1:
(B-Struct) B1≡B2 B2
−→µ B02 B01≡B02 B1
−→µ B01
We also know thatB0 =B10. By applying lemma 3.10 onΓ `B B1 . Γ0 and premise B1 ≡ B2 we have Γ `B B2 . Γ0. Applying the induction hypothesis on Γ `B B2 . Γ0 and premise B2 −→µ B20 we know Γ00 `B B20 . Γ0 where Γ00 = sideEffect(µ,Γ). Since the congruence relation is commutative we knowB20 ≡B10 from premiseB10 ≡B20. The thesis follows by applying lemma 3.10 on Γ00 `B B20 . Γ0 and premiseB20 ≡B10 where Γ00=sideEffect(µ,Γ).
3.3.4.2 Type Preservation at the Service Layer
Type preservation for processes are presented below followed by type preserva-tion for services.
Type Preservation for Processes
Consider a well-typed process P typed with respect to an environment Γ. As-sume there exists a processP0 such thatP −→µ P0. Then P0 is also well typed with respect to Γ:
Theorem 3.16 (Type Preservation for Processes)
IfΓ `P P andP −→µ P0 thenΓ `P P0
Proof. AssumeΓ `P P andP −→µ P0. The proof is done by induction on the derivation ofP −→µ P0.
Case S-Read
In this case, we knowP =B·t·m˜ for a process consisting of a behaviour B, a state tand a message queuem:˜
(S-Read) B
readt
−−−−→B0 B·t·m˜−→τ B0·t·m˜
We also know thatµ=τ andP0 =B0·t·m.˜
Applying the Inversion Lemma (Lemma 3.9) to Γ `P B·t·m˜ we know that it can only be typed using rule T-Process:
(T-Process) Γ,Γ0`BB .Γ00 Γ,Γ0`statet Γ,Γ0`queuem˜ @o.o@l:<O>∈Γ0∨o:<O>∈Γ0
Γ`PB·t·m˜ (3.20)
Applying theorem 3.13 on premiseΓ,Γ0 `B B .Γ00from 3.20 and premise B −−−−→readt B0 from S-Read we know Γ000 `B B0 . Γ00 where Γ000 = sideEffect(readt,Γ,Γ0) = Γ,Γ0by the definition ofsideEffect(3.12). Since we knowt0=tandm˜0 = ˜mby the form of S-Read, the thesis follows from applying T-Process onΓ `P B0·t·m˜ byΓ,Γ0 `B B0 . Γ00 and premise Γ,Γ0 `state t,Γ,Γ0 `queue m˜ and@o.o@l :<O>∈Γ0 ∨ o:<O>∈Γ0 from 3.20.
Case S-Send
The proof is similar to the proof for case S-Read.
(S-Send) B
νro@l(e)
−−−−−→B0 B·t·m˜−−−−−−−→νro@l(e(t)) B0·t·m˜
Case S-Exec
The proof is similar to the proof for case S-Read.
(S-Exec) B
(r,o)!x
−−−−→B0
B·t·m˜−−−−−−→(r,o)!x(t) B0·t·m˜
Case S-Get
In this case, we knowP =B·t·(r,o, t0) :: ˜mfor a process consisting of a behaviourB, a statet and a message queue(r,o, t0) :: ˜m:
(S-Get) B
r:o(x)
−−−→B0 B·t·(r,o,t0)::˜m −→τ B0·t←xt0·m˜
We also know thatµ=τ andP0=B0·t←xt0·m.˜
By applying the Inversion Lemma (Lemma 3.9) toΓ `P B·t·(r,o, t0) :: ˜m we know that it can only be typed by rule T-Process:
(T-Process) Γ,Γ00`BB .Γ000 Γ,Γ00`statet Γ,Γ00`queue(r,o,t0)::˜m @o.o@l:<O>∈Γ0∨o:<O>∈Γ00
Γ`PB·t·(r,o,t0)::˜m (3.21)
LetΓ0= Γ,Γ00. By applying the Preservation for Behavioural Layer Theo-rem (theoTheo-rem 3.13) on pTheo-remiseΓ,Γ00 `B B .Γ000from 3.21 and on premise B −−−−→r:o(x) B0 from S-Get we get:
IfΓ0 `B B . Γ000 (3.22) andB −−−−→r:o(x) B0
thenΓ0000`B0.Γ000
whereΓ0000=sideEffect(r:o(x),Γ0)
From the definition ofsideEffect (definition 3.12) we know that there exist two cases forΓ0000:
SubcaseΓ0000= Γ0
Lemma 3.17 If Γ `queue (r,o, t0) :: ˜m thenΓ `queue m.˜
Proof. The proof follows immediately from definition 3.8.
By Γ0 `queue (r,o, t0) :: ˜mfrom 3.21 and by lemma 3.17 we have:
Γ0 `queue m˜ (3.23)
and we know by definition 3.8 that data tree t0 fulfills the require-ments for operation odefined in environmentΓ0:
(o:<Ti>∈Γ0∨o:<Ti, To>∈Γ0)∧ `t0:Tt0∧Tt0 ≤Ti (3.24) From the definition of sideEffect (definition 3.12) we know that the input through operationois going to be stored in an existing variable, x, which type is a super type of the declared input type ofo:
x:Tx∈Γ0∧(o:<Ti>∈Γ0∨o:<Ti, To>∈Γ0)∧Ti≤Tx (3.25) Lemma 3.18 If x:Tx∈Γ0 thenr(x)∈Roots(Γ0)
Proof. The proof follows from the form of the typing system.
By lemma 3.18 applied on x : Tx ∈ Γ0 from 3.25 we get r(x) ∈ Roots(Γ0).
Since we have Γ0 `state tfrom 3.21 we know by definition 3.7 that
r(x) :Tr(x)∈Γ0∧ ` (r(x))(t) :T0∧T0≤Tr(x) (3.26) By 3.24 and 3.25 we knowTt0 ≤Ti≤Tx.
SinceTt0 ≤TxandT0 ≤Tr(x)andr(x)∈Roots(Γ0)then byΓ0 `state tfrom 3.21 we know by definition 3.7 that
∀a:Ta∈Roots(Γ0). `(a)(t←xt0) :T00∧T00≤Ta (3.27) Sincex∈Roots(Γ0)we know byΓ0 `state tfrom 3.21 that
∀a∈Roots(t). a∈Roots(Γ0) (3.28) by definition 3.7.
From 3.27 and 3.28 we have
Γ0 `state t←xt0 (3.29) The thesis follows from applying T-Process onΓ0`B0.Γ00from 3.22 and on 3.23 and 3.29.
Subcase Γ0000=upd(Γ0, x, Ti)
Since no variable type declaration is used from the environment when typing a message queue with respect to an environment then by Γ0 `queue (r,o, t0) :: ˜mfrom 3.21 and by lemma 3.17 we know:
Γ0000 `queue m˜ (3.30) We also know that data treet0 fulfills the requirements for operation odefined in environmentΓ0 as shown in 3.24.
From the definition ofsideEffect(definition 3.12) we know(o:<Ti>∈ Γ0000∨o: <Ti, To>∈ Γ0000). The environment is updated with a new pathx, which gets the same type as the declared type for the input part ofo. If part of the path to the leaf of xis missing, it is created with typevoid as basic type for each missing step.
By the definition ofsideEffect and 3.24 we know
t0:Tt0∧Γ0000 ` x:Ti∧Tt0 ≤Ti (3.31)
By the form of Γ0000 and lemma 3.18 we know r(x) ∈ Roots(Γ0000).
From r(x)∈Roots(Γ0000), 3.31, the definition of upd andΓ0 `state t from 3.21 we know:
∀a:Ta ∈Roots(Γ0000). `(a)(t←xt0) :T∧T ≤Ta (3.32) The difference between Γ0 and Γ0000 as well as t and t ←x t0 is that pathxand its subnodes are added. Therefore we have byΓ0 `state t from 3.21 that
∀a∈Roots(t←xt0). a∈Roots(Γ0000) (3.33) From 3.32 and 3.33 we know Γ0000 `state t←x t0. The thesis follows from applying T-Process onΓ0000`B0.Γ00from 3.22 and onΓ0000 `state
t←xt0 and 3.30.
Case S-Assign
In this case, we knowP =B·t·m˜ for a process consisting of a behaviour B, a state tand a message queuem:˜
(S-Assign) B
−−→x =e B0 B·t·m˜−→τ B0·txe(t)·m˜
We also know thatµ=τ andP0 =B0·txe(t)·m.˜
By applying the Inversion Lemma (Lemma 3.9) toΓ `P B·t·m˜ we know that it can only be typed by rule T-Process:
(T-Process) Γ,Γ0`BB .Γ000 Γ,Γ0`statet Γ,Γ0`queuem˜ @o.o@l:<O>∈Γ0∨o:<O>∈Γ0
Γ`PB·t·m˜ (3.34)
LetΓ0= Γ,Γ00. By applying the Preservation for Behavioural Layer Theo-rem (theoTheo-rem 3.13) on pTheo-remiseΓ,Γ0 `B B .Γ000from 3.34 and on premise B −−−→x =e B0 from S-Assign we get:
IfΓ0 `B B . Γ000 (3.35)
andB −−−→x =e B0 thenΓ0000`B0.Γ000
whereΓ0000=sideEffect(x =e,Γ0)
From the definition ofsideEffect (definition 3.12) we know that there exist two cases forΓ0000:
Subcase Γ0000= Γ0
From 3.34 we haveΓ0 `queue m. Since˜ Γ0000= Γ0 we must also have
Γ0000 `queue m˜ (3.36) From the definition of sideEffect (definition 3.12) we know that x already exists inΓ0 and that its basic type equals the basic type of expressione:
Γ0 ` e:Te∧x:Tx∈Γ0∧bt(Te) =bt(Tx) (3.37) We therefore have that
T =T0 where `r(x)(t) :T ∧ (r(x))(txe(t)) :T0 (3.38) Sincexis an existing path and by 3.38 and byΓ0 `state tfrom 3.34 we know by definition 3.7 that
Γ0 `state txe(t) (3.39) The thesis follows from applying T-Process onΓ0`B0.Γ000from 3.35 and on 3.36 and 3.39.
Subcase Γ0000=upd(Γ0, x, bt(Tx)
By definition 3.8 we know that when typing a message queue with respect to an environment no variable type declaration is used from the environment. We therefore have
Γ0000 `queue m˜ (3.40) From the definition ofsideEffect (definition 3.12) we knowΓ0000 ` x: bt(Te), whereΓ0 ` e:Te∧x /∈Γ0. The environment is updated with a new pathxwhich gets the basic type of the result of the evaluation of expressione. If part of the path to the leaf of xis missing, it is created with typevoid as basic type for each missing step.
By the form ofΓ0000 and by lemma 3.18 we knowr(x)∈Roots(Γ0000).
Fromr(x)∈Roots(Γ0000), the definition ofsideEffect, the definition of upd (definition 3.6) andΓ0 `state tfrom 3.34 we have:
∀a:Ta∈Roots(Γ0000). `a(txe(t)) :T∧T ≤Ta (3.41) The difference between Γ0 and Γ0000 as well as t and t x e(t) is that path xand all its subnodes are added. Therefore we have by Γ0 `state t from 3.34 that
∀a∈Roots(txe(t)). a∈Roots(Γ0000) (3.42) From 3.41 and 3.42 we knowΓ0000 `state txe(t). The thesis follows from applying T-Process onΓ0 `B0.Γ000from 3.35 and onΓ0000 `state
txe(t)and 3.40.
Case S-Wait
The proof is similar to the proof for case S-Get.
Case S-Par
The proof is straightforward because the typing of operations in an envi-ronment does not change.
Type Preservation for Services
Consider a well-typed serviceStyped with respect to an environmentΓ. Assume there exists a service S0 such that S −→µ S0. Then S0 is also well typed with respect toΓ:
Theorem 3.19 (Type Preservation for Services)
If Γ `S S andS −→µ S0 then Γ `S S0
Proof. Assume Γ `S S andS −→µ S0. The proof is done by induction on the derivation ofS −→µ S0.
Case S-Corr
In this case, we know S = B1 .DP | B2·t·m˜ for a behaviour B1, a deployment part D and a process consisting of a processP and another process with the behaviourB2, the statet and the message queuem:˜
(S-Corr) D=αC·Γ t
0,o`αCt (o:<Ti>∈Γ∨o:<Ti,To>∈Γ) `t0:Tt0 Tt0≤Ti
B1.DP |B2·t·m˜ νro(t 0)
−−−−−→B1.DP |B2·t·m˜::(r,o,t0)
We also know thatµ=νro(t0) andS0 =B1.DP |B2·t·m˜ :: (r,o, t0).
Applying the Inversion Lemma (Lemma 3.9) toΓ `S B1.DP |B2·t·m˜ we know that it can only be typed by rule T-Service:
(T-Service) D=αC·Γ ΓΓ``BSLB1.Γ0 Γ`PP |B2·t·m˜
SB1.DP |B2·t·m˜ (3.43) Applying the Inversion Lemma (Lemma 3.9) to premiseΓ `P P |B2·t·m˜
we know that it can only be typed by rule T-Process-Par:
(T-Process-Par) Γ`ΓP`P Γ`PB2·t·m˜
PP |B2·t·m˜ (3.44)
Applying the Inversion Lemma (Lemma 3.9) to premiseΓ `P B2·t·m˜ from this rule, we know that it can only be typed by rule T-Process:
(T-Process) Γ,Γ000`BB2.Γ0 Γ,Γ000`statet Γ,Γ000`queuem˜ @o.o@l:<O>∈Γ000∨o:<O>∈Γ000
Γ`PB2·t·m˜ (3.45)
Let Γ00 = Γ,Γ000. By premise Γ00 `queue m˜ from 3.45 and by premise (o : <Ti> ∈ Γ ∨ o : <Ti, To> ∈ Γ), ` t0 : Tt0 and Tt0 ≤ Ti from S-Corr we know that Γ00 `queue m˜ :: (r,o, t0) according to definition 3.8. By Γ00 `queue m˜ :: (r,o, t0) and premise Γ00 `B B2 . Γ0, Γ00 `state t and
@o.o@l:<O>∈Γ000 ∨ o:<O>∈Γ000 from 3.45 we can apply T-Process:
(T-Process) Γ,Γ000`BB2.Γ0 Γ,Γ000`statet Γ,Γ000`queuem˜::(r,o,t0) @o.o@l:<O>∈Γ000∨o:<O>∈Γ000 Γ`PB2·t·m˜::(r,o,t0)
(3.46) By applying T-Process-Par on premise Γ `P P from 3.44 and on Γ `P
B2·t·m:: (r,˜ o, t0)from 3.46 we get:
(T-Process-Par) Γ`ΓP`P Γ`PB2·t·m˜::(r,o,t0)
PP |B2·t·m˜::(r,o,t0) (3.47) The thesis follows from applying T-Service onΓ `P P|B2·t·m˜:: (r,o, t0)
from 3.47 and premiseD=αC·ΓandΓ `BSL B1 . Γ0 from 3.43.
Case S-Start
In this case, we knowS =B .DP for a behaviourB, a deployment part D and a processP:
(S-Start) D=αC·Γ t,o0αCP B
r:o(x)
−−−→B0 t0=init(t,o,αC) (o:<Ti>∈Γ∨o:<Ti,To>∈Γ) `t0:Tt0 Tt0≤Ti B.DP−−−−→νro(t) B.DP |B0·t⊥←xt←csetst0·
We also know thatµ=νro(t)andS0=B .DP |B0·t⊥←xt←csetst0·. Applying the Inversion Lemma (Lemma 3.9) to Γ `S B .DP we know that it can only be typed by rule T-Service:
(T-Service) D=αC·Γ Γ`Γ`BSLB .Γ0 Γ`PP
SB.DP (3.48)
Applying the Inversion Lemma (Lemma 3.9) to premise Γ `BSL B . Γ0 we know that it is typed either with T-BSL-Choice or T-BSL-Nil. Since a nil behaviour can not take a step of evaluation according to the semantics B must be a choice behaviour. Therefore can B only be typed using T-BSL-Choice.
(T-BSL-Choice) ∀j∈J .Γ`Bηj;Bj.Γj @Tk,Tl. x:Tk∈
SΓj∧x:Tl∈S
Γj∧Tk6=Tl Γ`BSLP
i∈J[ηi]{Bi}.S Γj∈J
Applying theorem 3.13 on premise Γ `B ηj;Bj . Γj from this rule and premise B −−−−→r:o(x) B0 from S-Start we get Γ00 `B B0 . Γ0 where Γ00 = sideEffect(x =e,Γ). Since Γ only contains operation type information we knowΓ00=upd(Γ, x, Ti)by the definition ofsideEffect (3.12).
ByΓ00and premise(o:<Ti>∈Γ∨o:<Ti, To>∈Γ),`t0 :Tt0 andTt0 ≤Ti from S-Start we have Γ00 `state t⊥ ←xt←csetst0 according to definition 3.7. By Γ00 we haveΓ00 `queue according to definition 3.8.
Let Γ,Γ000 = Γ00.By applying Γ,Γ000 `B B0 . Γ0, Γ,Γ000 `state t⊥ ←x t←csetst0 andΓ,Γ000 `queue on T-Process we get:
(T-Process) Γ,Γ000`BB0.Γ0 Γ,Γ000`statet⊥←xt←csetst0 Γ,Γ000`queue @o.o@l:<O>∈Γ000∨o:<O>∈Γ000 Γ`PB0·t⊥←xt←csetst0·
(3.49) By applying on T-process-par premise Γ `P P from 3.48 andΓ `P B0·
t⊥←xt←csetst0·from 3.49 we get:
(T-Process-Par) ΓΓ``PP Γ`PB0·t⊥←xt←csetst0·
PP |Γ`PB0·t⊥←xt←csetst0· (3.50)
The thesis follows from applying T-Service onB .DP |B0·t⊥←xt←csets t0·by conclusionΓ `P P |Γ `P B0·t⊥←xt←csetst0·from 3.50 and premiseD=αC·ΓandΓ `BSL B . Γ0 from 3.48:
(T-Service) D=αC·Γ ΓΓ``BB .Γ0 Γ`PP |Γ`PB0·t⊥←xt←csetst0·
SB.DP |B0·t⊥←xt←csetst0·
Case S-Send-Lift
If the last rule in the derivation sequence is S-Send-Lift, then from the form of this rule, we see thatS=B .DPfor a behaviourB, a deployment partD and a processP:
(S-Send-Lift) P
νro@l(t)
−−−−−→P0 B.DP−−−−−→νro@l(t) B.DP0
We also know that µ = νro@l(t) and S0 = B .DP0. Applying the Inversion Lemma (Lemma 3.9) toΓ `S B .DP we know that it can only be typed by rule T-Service:
(T-Service) D=αC·Γ ΓΓ``BSLB .Γ0 Γ`PP
SB.DP (3.51)
Applying theorem 3.16 on premiseΓ `P Pfrom 3.51 and premiseP −−−−−−→νro@l(t) P0 from S-Send-Lift we get Γ `P P0. The thesis follows from applying T-Service on Γ `S B .DP0 by Γ `P P0 and premise D = αC·Γ and Γ `BSL B . Γ0 from 3.51.
Case S-Exec-Lift
The proof is similar to the proof for case S-Send-Lift.
Case S-Wait-Lift
The proof is similar to the proof for case S-Send-Lift.
Case S-Tau
The proof is similar to the proof for case S-Send-Lift.