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