author | wenzelm |
Sat, 14 Jun 2008 23:19:51 +0200 | |
changeset 27208 | 5fe899199f85 |
parent 26351 | d5125a62f839 |
child 35068 | 544867142ea4 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: ProcedureInterface.thy |
|
17309 | 3 |
ID: $Id$ |
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
21624 | 6 |
*) |
3807 | 7 |
|
21624 | 8 |
header {* Procedure interface for RPC-Memory components *} |
3807 | 9 |
|
17309 | 10 |
theory ProcedureInterface |
26351 | 11 |
imports "../TLA" RPCMemoryParams |
17309 | 12 |
begin |
3807 | 13 |
|
17309 | 14 |
typedecl |
3807 | 15 |
(* type of channels with argument type 'a and return type 'r. |
17309 | 16 |
we model a channel as an array of variables (of type chan) |
17 |
rather than a single array-valued variable because the |
|
3807 | 18 |
notation gets a little simpler. |
19 |
*) |
|
20 |
('a,'r) chan |
|
17309 | 21 |
types |
22 |
('a,'r) channel =" (PrIds => ('a,'r) chan) stfun" |
|
3807 | 23 |
|
24 |
consts |
|
25 |
(* data-level functions *) |
|
17309 | 26 |
cbit :: "('a,'r) chan => bit" |
27 |
rbit :: "('a,'r) chan => bit" |
|
3807 | 28 |
arg :: "('a,'r) chan => 'a" |
29 |
res :: "('a,'r) chan => 'r" |
|
30 |
||
31 |
(* state functions *) |
|
17309 | 32 |
caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun" |
3807 | 33 |
rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun" |
34 |
||
35 |
(* state predicates *) |
|
36 |
Calling :: "('a,'r) channel => PrIds => stpred" |
|
37 |
||
38 |
(* actions *) |
|
6255 | 39 |
ACall :: "('a,'r) channel => PrIds => 'a stfun => action" |
40 |
AReturn :: "('a,'r) channel => PrIds => 'r stfun => action" |
|
3807 | 41 |
|
42 |
(* temporal formulas *) |
|
43 |
PLegalCaller :: "('a,'r) channel => PrIds => temporal" |
|
44 |
LegalCaller :: "('a,'r) channel => temporal" |
|
45 |
PLegalReturner :: "('a,'r) channel => PrIds => temporal" |
|
46 |
LegalReturner :: "('a,'r) channel => temporal" |
|
47 |
||
6255 | 48 |
(* slice through array-valued state function *) |
49 |
slice :: "('a => 'b) stfun => 'a => 'b stfun" |
|
50 |
||
51 |
syntax |
|
17309 | 52 |
"_slice" :: "[lift, 'a] => lift" ("(_!_)" [70,70] 70) |
6255 | 53 |
|
17309 | 54 |
"_Call" :: "['a, 'b, lift] => lift" ("(Call _ _ _)" [90,90,90] 90) |
55 |
"_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90) |
|
3807 | 56 |
|
6255 | 57 |
translations |
58 |
"_slice" == "slice" |
|
59 |
||
60 |
"_Call" == "ACall" |
|
61 |
"_Return" == "AReturn" |
|
62 |
||
17309 | 63 |
defs |
64 |
slice_def: "(PRED (x!i)) s == x s i" |
|
3807 | 65 |
|
17309 | 66 |
caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))" |
67 |
rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" |
|
3807 | 68 |
|
17309 | 69 |
Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" |
70 |
Call_def: "(ACT Call ch p v) == ACT ~ $Calling ch p |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
71 |
& (cbit<ch!p>$ ~= $rbit<ch!p>) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
72 |
& (arg<ch!p>$ = $v)" |
17309 | 73 |
Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
74 |
& (rbit<ch!p>$ = $cbit<ch!p>) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
75 |
& (res<ch!p>$ = $v)" |
17309 | 76 |
PLegalCaller_def: "PLegalCaller ch p == TEMP |
6255 | 77 |
Init(~ Calling ch p) |
78 |
& [][ ? a. Call ch p a ]_((caller ch)!p)" |
|
17309 | 79 |
LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
80 |
PLegalReturner_def: "PLegalReturner ch p == TEMP |
|
6255 | 81 |
[][ ? v. Return ch p v ]_((rtrner ch)!p)" |
17309 | 82 |
LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
83 |
||
21624 | 84 |
declare slice_def [simp] |
85 |
||
86 |
lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def |
|
87 |
PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def |
|
88 |
||
89 |
(* Calls and returns change their subchannel *) |
|
90 |
lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)" |
|
91 |
by (auto simp: angle_def Call_def caller_def Calling_def) |
|
92 |
||
93 |
lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)" |
|
94 |
by (auto simp: angle_def Return_def rtrner_def Calling_def) |
|
3807 | 95 |
|
96 |
end |