[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol Specification Kind Type
# .list-datafList('a) → Nat
#oclist-permf'a × List('a) → Nat
. 'listf'a → List('a)
. + .nat-basicfNat × Nat → Nat
. + .list-dataf'a × List('a) → List('a)
. + .listfList('a) × List('a) → List('a)
. + .listfList('a) × 'a → List('a)
. ++ .list-dupfList('a) × 'a → List('a)
. +1nat-basicfNat → Nat
. +2 .listf'a × 'a → List('a)
. - .natpfNat × Nat → Nat with λ n, m. n ≥ m
. -1nat-basicpfNat → Nat with λ n. n ≠ 0
. -1l .list-delfList('a) × 'a → List('a)
. -l .list-delfList('a) × 'a → List('a)
. -p .list-delfList('a) × Nat → List('a)
. .R?RWeventpRWevent
. .W?RWeventpRWevent
. .butlastlist-lastpfList('a) → List('a) with λ x. x ≠ []
. .count ( . )filter-countfList('a) × ('a → Bool) → Nat
. .count ( . )filter-countpfList('a) × Nat × Nat × ('a → Bool) → Nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
. .distinctlist-dupfList('a) → List('a)
. .drop ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .dropRight ( . )list-lastpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .exists ( . )forall-indexWherepList('a) × ('a → Type(Bool))
. .filter ( . )filter-countfList('a) × ('a → Bool) → List('a)
. .foldLeft ( . )listfList('a) × 'b × ('b × 'a → 'b) → 'b
. .forall ( . )forall-indexWherepList('a) × ('a → Type(Bool))
. .gstatePLIBfPLIBState → PLIBGState
. .gstate:= .PLIBfPLIBState × PLIBGState → PLIBState
. .hPLIBfPLIBGState → List((RWevent, Bool))
. .h:= .PLIBfPLIBGState × List((RWevent, Bool)) → PLIBGState
. .headlist-datapfList('a) → 'a with λ x. x ≠ []
. .ilPLIBfPLIBLState → L
. .il:= .PLIBfPLIBLState × L → PLIBLState
. .indexOf ( . )list-delfList('a) × 'a → Nat
. .indexWhere ( . )forall-indexWherefList('a) × ('a → Bool) → Nat
. .invAPersistlPLIBpfPLIBAction → L with λ a. ∃ l. a = globalAPersist(l)
. .ivPLIBfPLIBLState → V
. .iv:= .PLIBfPLIBLState × V → PLIBLState
. .lRWeventfRWevent → L
. .lPLIBpfPLIBAction → L with λ a. ∃ t, l. a = AInvRead(t, l)
. .lastlist-lastpfList('a) → 'a with λ x. x ≠ []
. .lastPersistedOrElse ( . )PLIB-predspList((RWevent, Bool)) × L × Bool
. .locPLIBpfPLIBAction → L with λ a. ∃ t, l, v. a = AInvWrite(t, l, v)
. .lsfPLIBfPLIBState → T → PLIBLState
. .lsf:= .PLIBfPLIBState × (T → PLIBLState) → PLIBState
. .map ( . )listfList('a) × ('a → 'b) → List('b)
. .ovPLIBfPLIBLState → V
. .ov:= .PLIBfPLIBLState × V → PLIBLState
. .pcfPLIBfPLIBState → T → PLIBPC
. .pcf:= .PLIBfPLIBState × (T → PLIBPC) → PLIBState
. .pmPLIBfPLIBGState → L → V
. .pm:= .PLIBfPLIBGState × (L → V) → PLIBGState
. .sublist ( . )list-delpfList('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .tRWeventfRWevent → T
. .tPLIBfPLIBLState → T
. .tPLIBpfPLIBAction → T with λ a. (∃ t. a = callTSync(t)) ∨ (∃ t. a = callARun(t)) ∨ (∃ t. a = ARetWrite(t)) ∨ (∃ t, v. a = ARetRead(t, v)) ∨ (∃ t, l, v. a = AInvWrite(t, l, v)) ∨ (∃ t, l. a = AInvRead(t, l)) ∨ (∃ t. a = ADoWrite(t)) ∨ (∃ t. a = ADoRead(t))
. .t:= .PLIBfPLIBLState × T → PLIBLState
. .taillist-datapfList('a) → List('a) with λ x. x ≠ []
. .take ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .takeRight ( . )list-delpfList('a) × Nat → List('a) with λ x, n. n ≤ # x
. .vRWeventfRWevent → V
. .vPLIBpfPLIBAction → V with λ a. ∃ t, v. a = ARetRead(t, v)
. .valPLIBpfPLIBAction → V with λ a. ∃ t, l, v. a = AInvWrite(t, l, v)
. .vmPLIBfPLIBGState → L → V
. .vm:= .PLIBfPLIBGState × (L → V) → PLIBGState
. < .nat-basicpNat × Nat
. < .list-datapList('a) × List('a)
. > .natpNat × Nat
. [ . := . ]list-getputpfList('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . ]list-getputpfList('a) × Nat → 'a with λ x, n. n < # x
. \ .list-setfList('a) × List('a) → List('a)
. | .PLIB-predsfList((RWevent, Bool)) × T → List((RWevent, Bool))
. | .PLIB-predsfList((RWevent, Bool)) × Bool → List((RWevent, Bool))
. | .PLIB-predsfList((RWevent, Bool)) × L → List((RWevent, Bool))
. |RPLIB-predsfList((RWevent, Bool)) → List((RWevent, Bool))
. |WPLIB-predsfList((RWevent, Bool)) → List((RWevent, Bool))
. ∈ .listp'a × List('a)
. ∪ .list-setfList('a) × List('a) → List('a)
. ≤ .natpNat × Nat
. ≥ .natpNat × Nat
. ⊆ .list-setpList('a) × List('a)
. ⊆m .list-permpList('a) × List('a)
. ⊑ .list-lastpList('a) × List('a)
. ⊑p .PLIB-predspList((RWevent, Bool)) × List((RWevent, Bool))
. ⊒ .list-lastpList('a) × List('a)
. ⊕ .PLIB-predsf(L → V) × List((RWevent, Bool)) → L → V
. intersect .list-setfList('a) × List('a) → List('a)
. zip .filter-countfList('a) × List('b) → List(('a, 'b))
[]list-datacList('a)
τPLIBcPLIBAction
∅memoryfL → V
ACrashPLIBpr(L → V) : (L → V) × List((RWevent, Bool)) × (T → PLIBPC)
ADOREADPLIBprT × L × (L → V) : V × List((RWevent, Bool))
ADoReadPLIBfT → PLIBAction
ADoWritePLIBfT → PLIBAction
AInvReadPLIBfT × L → PLIBAction
AInvWritePLIBfT × L × V → PLIBAction
APersistPLIBprL : (L → V) × List((RWevent, Bool))
ARETREADPLIBprV : : V
ARetReadPLIBfT × V → PLIBAction
ARetWritePLIBfT → PLIBAction
ARunPLIBpr :
DOWRITEPLIBprT × L × V : (L → V) × List((RWevent, Bool))
INVREADPLIBprL : L
INVWRITEPLIBprL × V : L × V
Lmemorys
Listlist-datas
Natnat-basics
OmemorycV
PLIBActionPLIBs
PLIBGInvPLIBpPLIBGState
PLIBGStatePLIBs
PLIBInvPLIBpPLIBGState × (T → Type(PLIBLState)) × (T → Type(PLIBPC))
PLIBLInvPLIBpPLIBGState × PLIBLState × PLIBPC
PLIBLStatePLIBs
PLIBPCPLIBs
PLIBRelyPLIBpPLIBGState × T × PLIBGState
PLIBStatePLIBs
RRWeventfT × L × V → RWevent
RETWRITEPLIBpr :
RWeventRWevents
Tmemorys
TSyncPLIBprT × List((RWevent, Bool)) :
Vmemorys
WRWeventfT × L × V → RWevent
aPLIB-proofsvPLIBAction
allReadsOKPLIB-predspList((RWevent, Bool))
allReadsOKIndPLIB-predsp(L → Type(V)) × (L → Type(Bool)) × List((RWevent, Bool))
allWritesOKPLIB-predspList((RWevent, Bool))
allWritesOKIndPLIB-predsp(T → Type(Bool)) × (L → Type(Bool)) × List((RWevent, Bool))
bPLIB-proofsvBool
callARunPLIBfT → PLIBAction
callTSyncPLIBfT → PLIBAction
crashedPLIBcPLIBPC
disjlist-duppList('a) × List('a)
dupslist-duppList('a)
ePLIB-proofsvRWevent
eventsPLIB-predsfList((RWevent, Bool)) → List(RWevent)
fillfirstlist-lastfNat × 'a × List('a) → List('a)
firstVolWritePLIB-predsfL × List((RWevent, Bool)) → Nat
fromelist-delfList('a) × 'a → List('a)
globalACrashPLIBcPLIBAction
globalAPersistPLIBfL → PLIBAction
gsPLIB-proofsvPLIBGState
gstatePLIB-proofsvPLIBGState
gstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBGState
hPLIB-proofsvList((RWevent, Bool))
idlePLIBcPLIBPC
ilPLIB-proofsvL
invAPersistlPLIB-proofsvL
invReadPLIBcPLIBPC
invWritePLIBcPLIBPC
ivPLIB-proofsvV
lPLIB-proofsvL
locPLIB-proofsvL
lsPLIB-proofsvPLIBLState
lsfPLIB-proofsvT → PLIBLState
lstepPLIBpPLIBGState × PLIBLState × PLIBPC × PLIBAction × PLIBGState × PLIBLState × PLIBPC
lstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBLState
mPLIB-proofsvNat
mkPLIBgsPLIBf(L → V) × (L → V) × List((RWevent, Bool)) → PLIBGState
mkPLIBlsPLIBfT × L × V × V → PLIBLState
mklistlist-lastf'a × Nat → List('a)
mkstatePLIBfPLIBGState × (T → PLIBLState) × (T → PLIBPC) → PLIBState
nPLIB-proofsvNat
ovPLIB-proofsvV
pcPLIB-proofsvPLIBPC
pcfPLIB-proofsvT → PLIBPC
pcstepfPLIBfPLIBGState × PLIBLState × PLIBPC × PLIBAction → PLIBPC
permlist-permpList('a) × List('a)
persistDependentReadsPLIB-predsfL × List((RWevent, Bool)) → List((RWevent, Bool))
plibInitPLIBpPLIBState
plibStepPLIBpPLIBState × PLIBAction × PLIBState
pmPLIB-proofsvL → V
prePLIBpPLIBGState × PLIBLState × PLIBPC × PLIBAction
readyPLIBcPLIBPC
relyPLIB-predspT × List((RWevent, Bool)) × List((RWevent, Bool))
resReadPLIBcPLIBPC
resWritePLIBcPLIBPC
revlist-lastfList('a) → List('a)
sPLIB-proofsvPLIBState
tPLIB-proofsvT
tidPLIB-proofsvT
vPLIB-proofsvV
valPLIB-proofsvV
vmPLIB-proofsvL → V
vpePLIB-proofsv(RWevent, Bool)