Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: RPC.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/TLA/Memory/RPC.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>RPC-Memory example: RPC specification\<close>

theory RPC
imports RPCParameters ProcedureInterface Memory
begin

type_synonym rpcSndChType = "(rpcOp,Vals) channel"
type_synonym rpcRcvChType = "memChType"
type_synonym rpcStType = "(PrIds \ rpcState) stfun"

(* state predicates *)

definition RPCInit :: "rpcRcvChType \ rpcStType \ PrIds \ stpred"
  where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \ \Calling rcv p)"

(* actions *)

definition RPCFwd :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ action"
  where "RPCFwd send rcv rst p == ACT
      $(Calling send p)
    \<and> $(rst!p) = # rpcA
    \<and> IsLegalRcvArg<arg<$(send!p)>>
    \<and> Call rcv p RPCRelayArg<arg<send!p>>
    \<and> (rst!p)$ = # rpcB
    \<and> unchanged (rtrner send!p)"

definition RPCReject :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ action"
  where "RPCReject send rcv rst p == ACT
      $(rst!p) = # rpcA
    \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
    \<and> Return send p #BadCall
    \<and> unchanged ((rst!p), (caller rcv!p))"

definition RPCFail :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ action"
  where "RPCFail send rcv rst p == ACT
      \<not>$(Calling rcv p)
    \<and> Return send p #RPCFailure
    \<and> (rst!p)$ = #rpcA
    \<and> unchanged (caller rcv!p)"

definition RPCReply :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ action"
  where "RPCReply send rcv rst p == ACT
      \<not>$(Calling rcv p)
    \<and> $(rst!p) = #rpcB
    \<and> Return send p res<rcv!p>
    \<and> (rst!p)$ = #rpcA
    \<and> unchanged (caller rcv!p)"

definition RPCNext :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ action"
  where "RPCNext send rcv rst p == ACT
    (  RPCFwd send rcv rst p
     \<or> RPCReject send rcv rst p
     \<or> RPCFail send rcv rst p
     \<or> RPCReply send rcv rst p)"

(* temporal *)

definition RPCIPSpec :: "rpcSndChType \ rpcRcvChType \ rpcStType \ PrIds \ temporal"
  where "RPCIPSpec send rcv rst p == TEMP
     Init RPCInit rcv rst p
   \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"

definition RPCISpec :: "rpcSndChType \ rpcRcvChType \ rpcStType \ temporal"
  where "RPCISpec send rcv rst == TEMP (\p. RPCIPSpec send rcv rst p)"

lemmas RPC_action_defs =
  RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def

lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def

(* The RPC component engages in an action for process p only if there is an outstanding,
   unanswered call for that process.
*)

lemma RPCidle: "\ \$(Calling send p) \ \RPCNext send rcv rst p"
  by (auto simp: AReturn_def RPC_action_defs)

lemma RPCbusy: "\ $(Calling rcv p) \ $(rst!p) = #rpcB \ \RPCNext send rcv rst p"
  by (auto simp: RPC_action_defs)

(* RPC failure actions are visible. *)
lemma RPCFail_vis: "\ RPCFail send rcv rst p \
    <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
  by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)

lemma RPCFail_Next_enabled: "\ Enabled (RPCFail send rcv rst p) \
    Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
  by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])

(* Enabledness of some actions *)
lemma RPCFail_enabled: "\p. basevars (rtrner send!p, caller rcv!p, rst!p) \
    \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCFail_def},
    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)

lemma RPCReply_enabled: "\p. basevars (rtrner send!p, caller rcv!p, rst!p) \
      \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB
         \<longrightarrow> Enabled (RPCReply send rcv rst p)"
  by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCReply_def},
    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)

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.