Impressum ProcedureInterface.thy Sprache: Isabelle

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

section \<open>Procedure interface for RPC-Memory components\<close>

theory ProcedureInterface
imports "HOL-TLA.TLA" RPCMemoryParams
begin

typedecl ('a,'r) chan
  (* type of channels with argument type 'a and return type 'r.
     we model a channel as an array of variables (of type chan)
     rather than a single array-valued variable because the
     notation gets a little simpler.
  *)
type_synonym ('a,'r) channel =" (PrIds \ ('a,'r) chan) stfun"

(* data-level functions *)

consts
  cbit          :: "('a,'r) chan \ bit"
  rbit          :: "('a,'r) chan \ bit"
  arg           :: "('a,'r) chan \ 'a"
  res           :: "('a,'r) chan \ 'r"

(* state functions *)

definition caller :: "('a,'r) channel \ (PrIds \ (bit * 'a)) stfun"
  where "caller ch == \s p. (cbit (ch s p), arg (ch s p))"

definition rtrner :: "('a,'r) channel \ (PrIds \ (bit * 'r)) stfun"
  where "rtrner ch == \s p. (rbit (ch s p), res (ch s p))"

(* slice through array-valued state function *)

definition slice :: "('a \ 'b) stfun \ 'a \ 'b stfun"
  where "slice x i s \ x s i"

syntax
  "_slice" :: "[lift, 'a] \ lift" (\(_!_)\ [70,70] 70)
translations
  "_slice" \<rightleftharpoons> "CONST slice"

(* state predicates *)

definition Calling :: "('a,'r) channel \ PrIds \ stpred"
  where "Calling ch p == PRED cbit< ch!p > \ rbit< ch!p >"

(* actions *)

definition ACall :: "('a,'r) channel \ PrIds \ 'a stfun \ action"
  where "ACall ch p v \ ACT
      \<not> $Calling ch p
    \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
    \<and> (arg<ch!p>$ = $v)"

definition AReturn :: "('a,'r) channel \ PrIds \ 'r stfun \ action"
  where "AReturn ch p v == ACT
      $Calling ch p
    \<and> (rbit<ch!p>$ = $cbit<ch!p>)
    \<and> (res<ch!p>$ = $v)"

syntax
  "_Call" :: "['a, 'b, lift] \ lift" (\(Call _ _ _)\ [90,90,90] 90)
  "_Return" :: "['a, 'b, lift] \ lift" (\(Return _ _ _)\ [90,90,90] 90)
translations
  "_Call" \<rightleftharpoons> "CONST ACall"
  "_Return" \<rightleftharpoons> "CONST AReturn"

(* temporal formulas *)

definition PLegalCaller :: "('a,'r) channel \ PrIds \ temporal"
  where "PLegalCaller ch p == TEMP
     Init(\<not> Calling ch p)
     \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"

definition LegalCaller :: "('a,'r) channel \ temporal"
  where "LegalCaller ch == TEMP (\p. PLegalCaller ch p)"

definition PLegalReturner :: "('a,'r) channel \ PrIds \ temporal"
  where "PLegalReturner ch p == TEMP \[\v. Return ch p v ]_((rtrner ch)!p)"

definition LegalReturner :: "('a,'r) channel \ temporal"
  where "LegalReturner ch == TEMP (\p. PLegalReturner ch p)"

declare slice_def [simp]

lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
  PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def

(* Calls and returns change their subchannel *)
lemma Call_changed: "\ Call ch p v \ _((caller ch)!p)"
  by (auto simp: angle_def ACall_def caller_def Calling_def)

lemma Return_changed: "\ Return ch p v \ _((rtrner ch)!p)"
  by (auto simp: angle_def AReturn_def rtrner_def Calling_def)

end

quality90%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.