src/HOL/TLA/Memory/ProcedureInterface.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        ProcedureInterface.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
   Theory Name: ProcedureInterface
wenzelm@3807
     7
   Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
   Procedure interface for RPC-Memory components.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@3807
    12
ProcedureInterface = TLA + RPCMemoryParams +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@3807
    15
  (* type of channels with argument type 'a and return type 'r.
wenzelm@3807
    16
     we model a channel as an array of variables (of type chan) 
wenzelm@3807
    17
     rather than a single array-valued variable because the 
wenzelm@3807
    18
     notation gets a little simpler.
wenzelm@3807
    19
  *)
wenzelm@3807
    20
  ('a,'r) chan
wenzelm@3807
    21
  ('a,'r) channel = (PrIds => ('a,'r) chan) stfun
wenzelm@3807
    22
wenzelm@3807
    23
arities
wenzelm@3807
    24
  chan :: (term,term) term
wenzelm@3807
    25
wenzelm@3807
    26
consts
wenzelm@3807
    27
  (* data-level functions *)
wenzelm@3807
    28
  cbit,rbit	:: "('a,'r) chan => bit"
wenzelm@3807
    29
  arg           :: "('a,'r) chan => 'a"
wenzelm@3807
    30
  res           :: "('a,'r) chan => 'r"
wenzelm@3807
    31
wenzelm@3807
    32
  (* state functions *)
wenzelm@3807
    33
  caller	:: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
wenzelm@3807
    34
  rtrner        :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
wenzelm@3807
    35
wenzelm@3807
    36
  (* state predicates *)
wenzelm@3807
    37
  Calling   :: "('a,'r) channel => PrIds => stpred"
wenzelm@3807
    38
wenzelm@3807
    39
  (* actions *)
wenzelm@6255
    40
  ACall      :: "('a,'r) channel => PrIds => 'a stfun => action"
wenzelm@6255
    41
  AReturn    :: "('a,'r) channel => PrIds => 'r stfun => action"
wenzelm@3807
    42
wenzelm@3807
    43
  (* temporal formulas *)
wenzelm@3807
    44
  PLegalCaller      :: "('a,'r) channel => PrIds => temporal"
wenzelm@3807
    45
  LegalCaller       :: "('a,'r) channel => temporal"
wenzelm@3807
    46
  PLegalReturner    :: "('a,'r) channel => PrIds => temporal"
wenzelm@3807
    47
  LegalReturner     :: "('a,'r) channel => temporal"
wenzelm@3807
    48
wenzelm@6255
    49
  (* slice through array-valued state function *)
wenzelm@6255
    50
  slice        :: "('a => 'b) stfun => 'a => 'b stfun"
wenzelm@6255
    51
wenzelm@6255
    52
syntax
wenzelm@6255
    53
  "_slice"     :: [lift, 'a] => lift       ("(_!_)" [70,70] 70)
wenzelm@6255
    54
wenzelm@6255
    55
  "_Call"     :: ['a, 'b, lift] => lift    ("(Call _ _ _)" [90,90,90] 90)
wenzelm@6255
    56
  "_Return"   :: ['a, 'b, lift] => lift    ("(Return _ _ _)" [90,90,90] 90)
wenzelm@3807
    57
wenzelm@6255
    58
translations
wenzelm@6255
    59
  "_slice"  ==  "slice"
wenzelm@6255
    60
wenzelm@6255
    61
  "_Call"   ==  "ACall"
wenzelm@6255
    62
  "_Return" ==  "AReturn"
wenzelm@6255
    63
wenzelm@6255
    64
rules
wenzelm@6255
    65
  slice_def     "(PRED (x!i)) s == x s i"
wenzelm@3807
    66
wenzelm@6255
    67
  caller_def	"caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
wenzelm@6255
    68
  rtrner_def	"rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
wenzelm@3807
    69
wenzelm@6255
    70
  Calling_def	"Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
wenzelm@6255
    71
  Call_def      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
wenzelm@6255
    72
                                     & (cbit<ch!p>` ~= $rbit<ch!p>)
wenzelm@6255
    73
                                     & (arg<ch!p>` = $v)"
wenzelm@6255
    74
  Return_def    "(ACT Return ch p v) == ACT  $Calling ch p
wenzelm@6255
    75
                                     & (rbit<ch!p>` = $cbit<ch!p>)
wenzelm@6255
    76
                                     & (res<ch!p>` = $v)"
wenzelm@6255
    77
  PLegalCaller_def      "PLegalCaller ch p == TEMP
wenzelm@6255
    78
                             Init(~ Calling ch p)
wenzelm@6255
    79
                             & [][ ? a. Call ch p a ]_((caller ch)!p)"
wenzelm@6255
    80
  LegalCaller_def       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
wenzelm@6255
    81
  PLegalReturner_def    "PLegalReturner ch p == TEMP
wenzelm@6255
    82
                                [][ ? v. Return ch p v ]_((rtrner ch)!p)"
wenzelm@6255
    83
  LegalReturner_def     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
wenzelm@3807
    84
wenzelm@3807
    85
end
wenzelm@3807
    86
wenzelm@6255
    87