author | wenzelm |
Wed, 07 Sep 2005 20:22:39 +0200 | |
changeset 17309 | c43ed29bd197 |
parent 12338 | de0f4a63baa5 |
child 21624 | 6f79647cf536 |
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 |
|
6 |
||
7 |
Theory Name: ProcedureInterface |
|
8 |
Logic Image: TLA |
|
9 |
||
10 |
Procedure interface for RPC-Memory components. |
|
11 |
*) |
|
12 |
||
17309 | 13 |
theory ProcedureInterface |
14 |
imports TLA RPCMemoryParams |
|
15 |
begin |
|
3807 | 16 |
|
17309 | 17 |
typedecl |
3807 | 18 |
(* type of channels with argument type 'a and return type 'r. |
17309 | 19 |
we model a channel as an array of variables (of type chan) |
20 |
rather than a single array-valued variable because the |
|
3807 | 21 |
notation gets a little simpler. |
22 |
*) |
|
23 |
('a,'r) chan |
|
17309 | 24 |
types |
25 |
('a,'r) channel =" (PrIds => ('a,'r) chan) stfun" |
|
3807 | 26 |
|
27 |
consts |
|
28 |
(* data-level functions *) |
|
17309 | 29 |
cbit :: "('a,'r) chan => bit" |
30 |
rbit :: "('a,'r) chan => bit" |
|
3807 | 31 |
arg :: "('a,'r) chan => 'a" |
32 |
res :: "('a,'r) chan => 'r" |
|
33 |
||
34 |
(* state functions *) |
|
17309 | 35 |
caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun" |
3807 | 36 |
rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun" |
37 |
||
38 |
(* state predicates *) |
|
39 |
Calling :: "('a,'r) channel => PrIds => stpred" |
|
40 |
||
41 |
(* actions *) |
|
6255 | 42 |
ACall :: "('a,'r) channel => PrIds => 'a stfun => action" |
43 |
AReturn :: "('a,'r) channel => PrIds => 'r stfun => action" |
|
3807 | 44 |
|
45 |
(* temporal formulas *) |
|
46 |
PLegalCaller :: "('a,'r) channel => PrIds => temporal" |
|
47 |
LegalCaller :: "('a,'r) channel => temporal" |
|
48 |
PLegalReturner :: "('a,'r) channel => PrIds => temporal" |
|
49 |
LegalReturner :: "('a,'r) channel => temporal" |
|
50 |
||
6255 | 51 |
(* slice through array-valued state function *) |
52 |
slice :: "('a => 'b) stfun => 'a => 'b stfun" |
|
53 |
||
54 |
syntax |
|
17309 | 55 |
"_slice" :: "[lift, 'a] => lift" ("(_!_)" [70,70] 70) |
6255 | 56 |
|
17309 | 57 |
"_Call" :: "['a, 'b, lift] => lift" ("(Call _ _ _)" [90,90,90] 90) |
58 |
"_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90) |
|
3807 | 59 |
|
6255 | 60 |
translations |
61 |
"_slice" == "slice" |
|
62 |
||
63 |
"_Call" == "ACall" |
|
64 |
"_Return" == "AReturn" |
|
65 |
||
17309 | 66 |
defs |
67 |
slice_def: "(PRED (x!i)) s == x s i" |
|
3807 | 68 |
|
17309 | 69 |
caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))" |
70 |
rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" |
|
3807 | 71 |
|
17309 | 72 |
Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" |
73 |
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
|
74 |
& (cbit<ch!p>$ ~= $rbit<ch!p>) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
75 |
& (arg<ch!p>$ = $v)" |
17309 | 76 |
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
|
77 |
& (rbit<ch!p>$ = $cbit<ch!p>) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
78 |
& (res<ch!p>$ = $v)" |
17309 | 79 |
PLegalCaller_def: "PLegalCaller ch p == TEMP |
6255 | 80 |
Init(~ Calling ch p) |
81 |
& [][ ? a. Call ch p a ]_((caller ch)!p)" |
|
17309 | 82 |
LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
83 |
PLegalReturner_def: "PLegalReturner ch p == TEMP |
|
6255 | 84 |
[][ ? v. Return ch p v ]_((rtrner ch)!p)" |
17309 | 85 |
LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
86 |
||
87 |
ML {* use_legacy_bindings (the_context ()) *} |
|
3807 | 88 |
|
89 |
end |