[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
# .set-basicfSet('a) → Nat
# .arrayfArray('a) → Nat
. % .nat-divpfNat × Nat → Nat with λ n, m. m ≠ 0
. * .nat-multfNat × Nat → Nat
. + .nat-basicfNat × Nat → Nat
. ++ .set-basicfSet('a) × 'a → Set('a)
. +1nat-basicfNat → Nat
. - .natpfNat × Nat → Nat with λ n, m. n ≥ m
. -1nat-basicpfNat → Nat with λ n. n ≠ 0
. .arHashsetfHashsetGState → Array(Elem)
. .ar:= .HashsetfHashsetGState × Array(Elem) → HashsetGState
. .bHashsetpHashsetLState
. .bSetppSetAction with λ a. (∃ tid, b. a = ARetMember(tid, b)) ∨ (∃ tid, b. a = ARetInsert(tid, b)) ∨ (∃ tid, b. a = ADoInsert(tid, b))
. .bHashsetppHashsetAction with λ a. ∃ tid, b. a = doINSERT(tid, b)
. .b:= .HashsetfHashsetLState × Bool → HashsetLState
. .eHashsetfHashsetLState → Elem
. .eSetpfSetAction → Elem with λ a. (∃ tid, e. a = AInvMember(tid, e)) ∨ (∃ tid, e. a = AInvInsert(tid, e))
. .e:= .HashsetfHashsetLState × Elem → HashsetLState
. .e0HashsetfHashsetLState → Elem
. .e0:= .HashsetfHashsetLState × Elem → HashsetLState
. .gstateSetfSetState → SetGState
. .gstateHashsetfHashsetState → HashsetGState
. .gstate:= .SetfSetState × SetGState → SetState
. .gstate:= .HashsetfHashsetState × HashsetGState → HashsetState
. .invINSERTeHashsetpfHashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invINSERT(tid, invINSERTe)
. .invMEMBEReHashsetpfHashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invMEMBER(tid, invINSERTe)
. .lbSetpSetLState
. .lb:= .SetfSetLState × Bool → SetLState
. .leSetfSetLState → Elem
. .le:= .SetfSetLState × Elem → SetLState
. .lsfSetfSetState → Tid → SetLState
. .lsfHashsetfHashsetState → Tid → HashsetLState
. .lsf:= .SetfSetState × (Tid → SetLState) → SetState
. .lsf:= .HashsetfHashsetState × (Tid → HashsetLState) → HashsetState
. .nHashsetfHashsetLState → Nat
. .n:= .HashsetfHashsetLState × Nat → HashsetLState
. .n0HashsetfHashsetLState → Nat
. .n0:= .HashsetfHashsetLState × Nat → HashsetLState
. .pcfSetfSetState → Tid → SetPC
. .pcfHashsetfHashsetState → Tid → HashsetPC
. .pcf:= .SetfSetState × (Tid → SetPC) → SetState
. .pcf:= .HashsetfHashsetState × (Tid → HashsetPC) → HashsetState
. .retINSERTbHashsetppHashsetAction with λ a. ∃ tid, b. a = retINSERT(tid, b)
. .retMEMBERbHashsetppHashsetAction with λ a. ∃ tid, b. a = retMEMBER(tid, b)
. .setSetfSetGState → Set(Elem)
. .set:= .SetfSetGState × Set(Elem) → SetGState
. .szHashsetfHashsetLState → Nat
. .sz:= .HashsetfHashsetLState × Nat → HashsetLState
. .tidSetfSetLState → Tid
. .tidHashsetfHashsetLState → Tid
. .tidSetpfSetAction → Tid with λ a. a ≠ τ
. .tidHashsetpfHashsetAction → Tid with λ a. a ≠ τ
. .tid:= .SetfSetLState × Tid → SetLState
. .tid:= .HashsetfHashsetLState × Tid → HashsetLState
. / .nat-divpfNat × Nat → Nat with λ n, m. m ≠ 0
. < .nat-basicpNat × Nat
. > .natpNat × Nat
. [ . := . ]arraypfArray('a) × Nat × 'a → Array('a) with λ ar, n, a. n < # ar
. [ . ]arraypfArray('a) × Nat → 'a with λ ar, n. n < # ar
. ∈ .set-basicp'a × Set('a)
. ≤ .natpNat × Nat
. ≥ .natpNat × Nat
. ⊆ .set-basicpSet('a) × Set('a)
τSetcSetAction
τHashsetcHashsetAction
∅set-basiccSet('a)
⊥SetcElem
ADoInsertSetfTid × Bool → SetAction
ADoMemberSetfTid → SetAction
AInvInsertSetfTid × Elem → SetAction
AInvMemberSetfTid × Elem → SetAction
ARetInsertSetfTid × Bool → SetAction
ARetMemberSetfTid × Bool → SetAction
Arrayarrays
DOINSERTSetprBool × Elem : Bool × Set(Elem)
DOMEMBERSetprElem × Set(Elem) : Bool
ElemSets
HashsetActionHashsets
HashsetGInvHashsetpHashsetGState
HashsetGStateHashsets
HashsetInvHashsetpHashsetGState × (Tid → Type(HashsetLState)) × (Tid → Type(HashsetPC))
HashsetLInvHashsetpHashsetGState × HashsetLState × HashsetPC
HashsetLStateHashsets
HashsetPCHashsets
HashsetRelyHashsetpHashsetGState × Tid × HashsetGState
HashsetStateHashsets
I1HashsetcHashsetPC
I10HashsetcHashsetPC
I11HashsetcHashsetPC
I12HashsetcHashsetPC
I13HashsetcHashsetPC
I14HashsetcHashsetPC
I15HashsetcHashsetPC
I16HashsetcHashsetPC
I17HashsetcHashsetPC
I18HashsetcHashsetPC
I19HashsetcHashsetPC
I2HashsetcHashsetPC
I20HashsetcHashsetPC
I21HashsetcHashsetPC
I3HashsetcHashsetPC
I4HashsetcHashsetPC
I5HashsetcHashsetPC
I6HashsetcHashsetPC
I7HashsetcHashsetPC
I8HashsetcHashsetPC
I9HashsetcHashsetPC
INVINSERTSetprElem : Elem
INVMEMBERSetprElem : Elem
M1HashsetcHashsetPC
M10HashsetcHashsetPC
M11HashsetcHashsetPC
M12HashsetcHashsetPC
M13HashsetcHashsetPC
M14HashsetcHashsetPC
M15HashsetcHashsetPC
M16HashsetcHashsetPC
M17HashsetcHashsetPC
M18HashsetcHashsetPC
M2HashsetcHashsetPC
M3HashsetcHashsetPC
M4HashsetcHashsetPC
M5HashsetcHashsetPC
M6HashsetcHashsetPC
M7HashsetcHashsetPC
M8HashsetcHashsetPC
M9HashsetcHashsetPC
Natnat-basics
RETINSERTSetprBool : : Bool
RETMEMBERSetprBool : : Bool
Setset-basics
SetActionSets
SetGInvSetpSetGState
SetGStateSets
SetInvSetpSetGState × (Tid → Type(SetLState)) × (Tid → Type(SetPC))
SetLInvSetpSetGState × SetLState × SetPC
SetLStateSets
SetPCSets
SetRelySetpSetGState × Tid × SetGState
SetStateSets
Tidtids
aHashset-refines-SetvHashsetAction
aaHashset-refines-SetvSetAction
absHashset-refines-SetpHashsetState × SetState
abssetabspArray(Elem) × Set(Elem)
agsHashset-refines-SetvSetGState
allslotsfullhashset-predspArray(Elem) × Nat × Nat × Elem × Bool
alsHashset-refines-SetvSetLState
alsfHashset-refines-SetvTid → SetLState
apcHashset-refines-SetvSetPC
apcfHashset-refines-SetvTid → SetPC
arHashset-refines-SetvArray(Elem)
asHashset-refines-SetvSetState
bHashset-refines-SetvBool
betweenhashset-predspNat × Nat × Nat × Bool
doINSERTHashsetfTid × Bool → HashsetAction
doMEMBERHashsetfTid → HashsetAction
dummytidtidcTid
eHashset-refines-SetvElem
gabsHashset-refines-SetpHashsetGState × (Tid → Type(HashsetLState)) × (Tid → Type(HashsetPC)) × SetGState × (Tid → Type(SetLState)) × (Tid → Type(SetPC))
get_hashhashset-predsfElem × Nat → Nat
gsHashset-refines-SetvHashsetGState
gstepfSetfSetGState × SetLState × SetPC × SetAction → SetGState
gstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState
hashsetInitHashsetpHashsetState
hashsetStepHashsetpHashsetState × HashsetAction × HashsetState
htokhashset-predspArray(Elem)
idleSetcSetPC
idleHashsetcHashsetPC
invINSERTHashsetfTid × Elem → HashsetAction
invInsertSetcSetPC
invMEMBERHashsetfTid × Elem → HashsetAction
invMemberSetcSetPC
labsHashset-refines-SetpHashsetGState × HashsetLState × HashsetPC × SetGState × SetLState × SetPC
lbHashset-refines-SetvBool
leHashset-refines-SetvElem
lsHashset-refines-SetvHashsetLState
lsfHashset-refines-SetvTid → HashsetLState
lstepSetpSetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC
lstepHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC
lstepfSetfSetGState × SetLState × SetPC × SetAction → SetLState
lstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState
mkarhashset-predsfNat × Elem → Array(Elem)
mkarrayarrayfNat → Array('a)
mkarrayarrayfNat × 'a → Array('a)
mkgsSetfSet(Elem) → SetGState
mkgsHashsetfArray(Elem) → HashsetGState
mklsSetfTid × Elem × Bool → SetLState
mklsHashsetfTid × Elem × Bool × Nat × Nat × Nat × Elem → HashsetLState
mkstateSetfSetGState × (Tid → SetLState) × (Tid → SetPC) → SetState
mkstateHashsetfHashsetGState × (Tid → HashsetLState) × (Tid → HashsetPC) → HashsetState
nHashset-refines-SetvNat
pcHashset-refines-SetvHashsetPC
pcfHashset-refines-SetvTid → HashsetPC
pcstepfSetfSetGState × SetLState × SetPC × SetAction → SetPC
pcstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC
preSetpSetGState × SetLState × SetPC × SetAction
preHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction
relyhashset-predspArray(Elem) × Array(Elem)
renHashset-refines-SetfHashsetAction × SetGState × (Tid → SetLState) → SetAction
retINSERTHashsetfTid × Bool → HashsetAction
retInsertSetcSetPC
retMEMBERHashsetfTid × Bool → HashsetAction
retMemberSetcSetPC
sHashset-refines-SetvHashsetState
setHashset-refines-SetvSet(Elem)
setInitSetpSetState
setStepSetpSetState × SetAction × SetState
tidHashset-refines-SetvTid