src/HOL/TLA/Memory/RPCParameters.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:        RPCParameters.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: RPCParameters
     7     Logic Image: TLA
     8 
     9     RPC-Memory example: RPC parameters
    10     For simplicity, specify the instance of RPC that is used in the
    11     memory implementation.
    12 *)
    13 
    14 RPCParameters = MemoryParameters +
    15 
    16 datatype  rpcOp = memcall memOp | othercall Vals
    17 datatype  rpcState = rpcA | rpcB
    18 
    19 (***
    20 types
    21   (* type of RPC arguments other than memory calls *)
    22   noMemArgType
    23   (* legal arguments for (our instance of) the RPC component *)
    24   rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)"
    25 
    26 arities
    27   noMemArgType :: term
    28 ***)
    29 
    30 consts
    31   (* some particular return values *)
    32   RPCFailure     :: Vals
    33   BadCall        :: Vals
    34   
    35   (* Translate an rpc call to a memory call and test if the current argument
    36      is legal for the receiver (i.e., the memory). This can now be a little
    37      simpler than for the generic RPC component. RelayArg returns an arbitrary
    38      memory call for illegal arguments. *)
    39 (***
    40   IsLegalRcvArg  :: rpcArgType => bool
    41   RPCRelayArg    :: rpcArgType => memArgType
    42 ***)
    43   IsLegalRcvArg  :: rpcOp => bool
    44   RPCRelayArg    :: rpcOp => memOp
    45 
    46 rules
    47   (* RPCFailure is different from MemVals and exceptions *)
    48   RFNoMemVal        "RPCFailure ~: MemVal"
    49   NotAResultNotRF   "NotAResult ~= RPCFailure"
    50   OKNotRF           "OK ~= RPCFailure"
    51   BANotRF           "BadArg ~= RPCFailure"
    52 
    53 (***
    54   IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)"
    55   RPCRelayArg_def   "RPCRelayArg ra == 
    56                          case ra of Inl (rm) => (snd rm)
    57                                   | Inr (rn) => (read, @ l. True)"
    58 ***)
    59 defs
    60   IsLegalRcvArg_def "IsLegalRcvArg ra ==
    61 		         case ra of (memcall m) => True
    62 		                  | (othercall v) => False"
    63   RPCRelayArg_def   "RPCRelayArg ra ==
    64 		         case ra of (memcall m) => m
    65 		                  | (othercall v) => arbitrary"
    66 end
    67 
    68