|
(* Title: HOL/TLA/Memory/RPCParameters.thy
Author: Stephan Merz, University of Munich
*)
section \<open>RPC-Memory example: RPC parameters\<close>
theory RPCParameters
imports MemoryParameters
begin
(*
For simplicity, specify the instance of RPC that is used in the
memory implementation.
*)
datatype rpcOp = memcall memOp | othercall Vals
datatype rpcState = rpcA | rpcB
axiomatization RPCFailure :: Vals and BadCall :: Vals
where
(* RPCFailure is different from MemVals and exceptions *)
RFNoMemVal: "RPCFailure \ MemVal" and
NotAResultNotRF: "NotAResult \ RPCFailure" and
OKNotRF: "OK \ RPCFailure" and
BANotRF: "BadArg \ RPCFailure"
(* Translate an rpc call to a memory call and test if the current argument
is legal for the receiver (i.e., the memory). This can now be a little
simpler than for the generic RPC component. RelayArg returns an arbitrary
memory call for illegal arguments. *)
definition IsLegalRcvArg :: "rpcOp \ bool"
where "IsLegalRcvArg ra ==
case ra of (memcall m) \<Rightarrow> True
| (othercall v) \<Rightarrow> False"
definition RPCRelayArg :: "rpcOp \ memOp"
where "RPCRelayArg ra ==
case ra of (memcall m) \<Rightarrow> m
| (othercall v) \<Rightarrow> undefined"
lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
end
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
