Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: RPCParameters.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.