products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: RPC.thy   Sprache: Unknown

(*  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.24 Sekunden  (vorverarbeitet)  ]