isabelle: src/HOL/TLA/Memory/RPC.thy@68400ff46b09 (annotated)

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: RPC.thy
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	3	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6	Theory Name: RPC
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9	RPC-Memory example: RPC specification
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	12	RPC = RPCParameters + ProcedureInterface + Memory +
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	13
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14	types
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	15	rpcSndChType = "(rpcOp,Vals) channel"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	16	rpcRcvChType = "memChType"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17	rpcStType = "(PrIds => rpcState) stfun"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20	(* state predicates *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	RPCInit :: "rpcRcvChType => rpcStType => PrIds => stpred"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	22
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	23	(* actions *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24	RPCFwd :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	RPCReject :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	RPCFail :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	27	RPCReply :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	28	RPCNext :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	29
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	30	(* temporal *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	31	RPCIPSpec :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32	RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	33
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	34	rules
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	35	RPCInit_def "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	36
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	37	RPCFwd_def "RPCFwd send rcv rst p == ACT
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	38	$(Calling send p)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	39	& $(rst!p) = # rpcA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	40	& IsLegalRcvArg<arg<$(send!p)>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	41	& Call rcv p RPCRelayArg<arg<send!p>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	42	& (rst!p)$ = # rpcB
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	43	& unchanged (rtrner send!p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	44
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	45	RPCReject_def "RPCReject send rcv rst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	46	$(rst!p) = # rpcA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	47	& ~IsLegalRcvArg<arg<$(send!p)>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	48	& Return send p #BadCall
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	49	& unchanged ((rst!p), (caller rcv!p))"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	50
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	51	RPCFail_def "RPCFail send rcv rst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	52	~$(Calling rcv p)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	53	& Return send p #RPCFailure
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	54	& (rst!p)$ = #rpcA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	55	& unchanged (caller rcv!p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	56
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	57	RPCReply_def "RPCReply send rcv rst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	58	~$(Calling rcv p)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	59	& $(rst!p) = #rpcB
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	60	& Return send p res<rcv!p>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	61	& (rst!p)$ = #rpcA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	62	& unchanged (caller rcv!p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	63
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	64	RPCNext_def "RPCNext send rcv rst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	65	( RPCFwd send rcv rst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	66	\| RPCReject send rcv rst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	67	\| RPCFail send rcv rst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	68	\| RPCReply send rcv rst p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	69
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	70	RPCIPSpec_def "RPCIPSpec send rcv rst p == TEMP
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	71	Init RPCInit rcv rst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	72	& [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	73	& WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	74
9517 f58863b1406a tuned version by Stephan Merz (unbatchified etc.); wenzelm parents: 6255 diff changeset	75	RPCISpec_def "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	76
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	77	end
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	78
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	79
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	80

author	wenzelm
	Thu, 10 Aug 2000 00:45:23 +0200
changeset 9569	68400ff46b09
parent 9517	f58863b1406a
child 11703	6e5de8d4290a
permissions	-rw-r--r--