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