|
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 |
|
24 chan :: (term,term) term |
|
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 (* slice through array-valued state function *) |
|
33 "@" :: "('a => 'b) stfun => 'a => 'b stfun" (infixl 20) |
|
34 |
|
35 (* state functions *) |
|
36 caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun" |
|
37 rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun" |
|
38 |
|
39 (* state predicates *) |
|
40 Calling :: "('a,'r) channel => PrIds => stpred" |
|
41 |
|
42 (* actions *) |
|
43 Call :: "('a,'r) channel => PrIds => 'a trfct => action" |
|
44 Return :: "('a,'r) channel => PrIds => 'r trfct => action" |
|
45 |
|
46 (* temporal formulas *) |
|
47 PLegalCaller :: "('a,'r) channel => PrIds => temporal" |
|
48 LegalCaller :: "('a,'r) channel => temporal" |
|
49 PLegalReturner :: "('a,'r) channel => PrIds => temporal" |
|
50 LegalReturner :: "('a,'r) channel => temporal" |
|
51 |
|
52 rules |
|
53 slice_def "(x@i) s == x s i" |
|
54 |
|
55 caller_def "caller ch s p == (cbit (ch s p), arg (ch s p))" |
|
56 rtrner_def "rtrner ch s p == (rbit (ch s p), res (ch s p))" |
|
57 |
|
58 Calling_def "$(Calling ch p) .= (cbit[$(ch@p)] .~= rbit[$(ch@p)])" |
|
59 Call_def "Call ch p v == .~ $(Calling ch p) |
|
60 .& (cbit[$(ch@p)])` .~= rbit[$(ch@p)] |
|
61 .& (arg[$(ch@p)])` .= v" |
|
62 Return_def "Return ch p v == $(Calling ch p) |
|
63 .& (rbit[$(ch@p)])` .= cbit[$(ch@p)] |
|
64 .& (res[$(ch@p)])` .= v" |
|
65 |
|
66 PLegalCaller_def "PLegalCaller ch p == |
|
67 Init(.~ $(Calling ch p)) |
|
68 .& [][ REX a. Call ch p (#a) ]_((caller ch)@p)" |
|
69 LegalCaller_def "LegalCaller ch == RALL p. PLegalCaller ch p" |
|
70 PLegalReturner_def "PLegalReturner ch p == |
|
71 [][ REX v. Return ch p (#v) ]_((rtrner ch)@p)" |
|
72 LegalReturner_def "LegalReturner ch == RALL p. PLegalReturner ch p" |
|
73 |
|
74 end |
|
75 |