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