--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Memory/Memory.thy Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,137 @@
+(*
+ File: Memory.thy
+ Author: Stephan Merz
+ Copyright: 1997 University of Munich
+
+ Theory Name: Memory
+ Logic Image: TLA
+
+ RPC-Memory example: Memory specification
+*)
+
+Memory = MemoryParameters + ProcedureInterface +
+
+types
+ memChType = "(memArgType,Vals) channel"
+ memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *)
+ resType = "(PrIds => Vals) stfun"
+
+consts
+ (* state predicates *)
+ MInit :: "memType => Locs => stpred"
+ PInit :: "resType => PrIds => stpred"
+ (* auxiliary predicates: is there a pending read/write request for
+ some process id and location/value? *)
+ RdRequest :: "memChType => PrIds => Locs => stpred"
+ WrRequest :: "memChType => PrIds => Locs => Vals => stpred"
+
+ (* actions *)
+ GoodRead :: "memType => resType => PrIds => Locs => action"
+ BadRead :: "memType => resType => PrIds => Locs => action"
+ ReadInner :: "memChType => memType => resType => PrIds => Locs => action"
+ Read :: "memChType => memType => resType => PrIds => action"
+ GoodWrite :: "memType => resType => PrIds => Locs => Vals => action"
+ BadWrite :: "memType => resType => PrIds => Locs => Vals => action"
+ WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action"
+ Write :: "memChType => memType => resType => PrIds => Locs => action"
+ MemReturn :: "memChType => resType => PrIds => action"
+ MemFail :: "memChType => resType => PrIds => action"
+ RNext :: "memChType => memType => resType => PrIds => action"
+ UNext :: "memChType => memType => resType => PrIds => action"
+
+ (* temporal formulas *)
+ RPSpec :: "memChType => memType => resType => PrIds => temporal"
+ UPSpec :: "memChType => memType => resType => PrIds => temporal"
+ MSpec :: "memChType => memType => resType => Locs => temporal"
+ IRSpec :: "memChType => memType => resType => temporal"
+ IUSpec :: "memChType => memType => resType => temporal"
+
+ RSpec :: "memChType => resType => temporal"
+ USpec :: "memChType => temporal"
+
+ (* memory invariant: in the paper, the invariant is hidden in the definition of
+ the predicate S used in the implementation proof, but it is easier to verify
+ at this level. *)
+ MemInv :: "memType => Locs => stpred"
+
+rules
+ MInit_def "$(MInit mm l) .= ($(mm@l) .= # InitVal)"
+ PInit_def "$(PInit rs p) .= ($(rs@p) .= # NotAResult)"
+
+ RdRequest_def "$(RdRequest ch p l) .=
+ ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))))"
+ WrRequest_def "$(WrRequest ch p l v) .=
+ ($(Calling ch p) .& (arg[$(ch@p)] .= #(Inr (write,l,v))))"
+ (* a read that doesn't raise BadArg *)
+ GoodRead_def "GoodRead mm rs p l ==
+ #(MemLoc l) .& (rs@p)$ .= $(mm@l)"
+ (* a read that raises BadArg *)
+ BadRead_def "BadRead mm rs p l ==
+ .~ #(MemLoc l) .& (rs@p)$ .= #BadArg"
+ (* the read action with l visible *)
+ ReadInner_def "ReadInner ch mm rs p l ==
+ $(RdRequest ch p l)
+ .& (GoodRead mm rs p l .| BadRead mm rs p l)
+ .& unchanged (rtrner ch @ p)"
+ (* the read action with l quantified *)
+ Read_def "Read ch mm rs p == REX l. ReadInner ch mm rs p l"
+
+ (* similar definitions for the write action *)
+ GoodWrite_def "GoodWrite mm rs p l v ==
+ #(MemLoc l) .& #(MemVal v)
+ .& (mm@l)$ .= #v .& (rs@p)$ .= #OK"
+ BadWrite_def "BadWrite mm rs p l v ==
+ .~ (#(MemLoc l) .& #(MemVal v))
+ .& (rs@p)$ .= #BadArg .& unchanged (mm@l)"
+ WriteInner_def "WriteInner ch mm rs p l v ==
+ $(WrRequest ch p l v)
+ .& (GoodWrite mm rs p l v .| BadWrite mm rs p l v)
+ .& unchanged (rtrner ch @ p)"
+ Write_def "Write ch mm rs p l == REX v. WriteInner ch mm rs p l v"
+
+ (* the return action *)
+ MemReturn_def "MemReturn ch rs p ==
+ $(rs@p) .~= #NotAResult
+ .& (rs@p)$ .= #NotAResult
+ .& Return ch p ($(rs@p))"
+ (* the failure action of the unreliable memory *)
+ MemFail_def "MemFail ch rs p ==
+ $(Calling ch p)
+ .& (rs@p)$ .= #MemFailure
+ .& unchanged (rtrner ch @ p)"
+ RNext_def "RNext ch mm rs p ==
+ Read ch mm rs p
+ .| (REX l. Write ch mm rs p l)
+ .| MemReturn ch rs p"
+ UNext_def "UNext ch mm rs p ==
+ RNext ch mm rs p .| MemFail ch rs p"
+
+ RPSpec_def "RPSpec ch mm rs p ==
+ Init($(PInit rs p))
+ .& [][ RNext ch mm rs p ]_<rtrner ch @ p, rs@p>
+ .& WF(RNext ch mm rs p)_<rtrner ch @ p, rs@p>
+ .& WF(MemReturn ch rs p)_<rtrner ch @ p, rs@p>"
+ UPSpec_def "UPSpec ch mm rs p ==
+ Init($(PInit rs p))
+ .& [][ UNext ch mm rs p ]_<rtrner ch @ p, rs@p>
+ .& WF(RNext ch mm rs p)_<rtrner ch @ p, rs@p>
+ .& WF(MemReturn ch rs p)_<rtrner ch @ p, rs@p>"
+ MSpec_def "MSpec ch mm rs l ==
+ Init($(MInit mm l))
+ .& [][ REX p. Write ch mm rs p l ]_(mm@l)"
+ IRSpec_def "IRSpec ch mm rs ==
+ (RALL p. RPSpec ch mm rs p)
+ .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)"
+ IUSpec_def "IUSpec ch mm rs ==
+ (RALL p. UPSpec ch mm rs p)
+ .& (RALL l. #(MemLoc l) .-> MSpec ch mm rs l)"
+
+ RSpec_def "RSpec ch rs == EEX mm. IRSpec ch mm rs"
+ USpec_def "USpec ch == EEX mm rs. IUSpec ch mm rs"
+
+ MemInv_def "$(MemInv mm l) .=
+ (#(MemLoc l) .-> MemVal[ $(mm@l)])"
+end
+
+
+