|
3807
|
1 |
(*
|
|
|
2 |
File: RPCParameters.thy
|
|
|
3 |
Author: Stephan Merz
|
|
|
4 |
Copyright: 1997 University of Munich
|
|
|
5 |
|
|
|
6 |
Theory Name: RPCParameters
|
|
|
7 |
Logic Image: TLA
|
|
|
8 |
|
|
|
9 |
RPC-Memory example: RPC parameters
|
|
|
10 |
For simplicity, specify the instance of RPC that is used in the
|
|
|
11 |
memory implementation.
|
|
|
12 |
*)
|
|
|
13 |
|
|
|
14 |
RPCParameters = MemoryParameters +
|
|
|
15 |
|
|
6255
|
16 |
datatype rpcOp = memcall memOp | othercall Vals
|
|
3807
|
17 |
datatype rpcState = rpcA | rpcB
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
(* some particular return values *)
|
|
6255
|
21 |
RPCFailure :: Vals
|
|
|
22 |
BadCall :: Vals
|
|
3807
|
23 |
|
|
|
24 |
(* Translate an rpc call to a memory call and test if the current argument
|
|
|
25 |
is legal for the receiver (i.e., the memory). This can now be a little
|
|
|
26 |
simpler than for the generic RPC component. RelayArg returns an arbitrary
|
|
|
27 |
memory call for illegal arguments. *)
|
|
6255
|
28 |
IsLegalRcvArg :: rpcOp => bool
|
|
|
29 |
RPCRelayArg :: rpcOp => memOp
|
|
3807
|
30 |
|
|
|
31 |
rules
|
|
|
32 |
(* RPCFailure is different from MemVals and exceptions *)
|
|
6255
|
33 |
RFNoMemVal "RPCFailure ~: MemVal"
|
|
3807
|
34 |
NotAResultNotRF "NotAResult ~= RPCFailure"
|
|
|
35 |
OKNotRF "OK ~= RPCFailure"
|
|
|
36 |
BANotRF "BadArg ~= RPCFailure"
|
|
|
37 |
|
|
6255
|
38 |
defs
|
|
|
39 |
IsLegalRcvArg_def "IsLegalRcvArg ra ==
|
|
|
40 |
case ra of (memcall m) => True
|
|
|
41 |
| (othercall v) => False"
|
|
|
42 |
RPCRelayArg_def "RPCRelayArg ra ==
|
|
|
43 |
case ra of (memcall m) => m
|
|
|
44 |
| (othercall v) => arbitrary"
|
|
3807
|
45 |
end
|