[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
# .	heap	f	Heap[A] → Nat
# .	set-basic	f	Set[A] → Nat
. ( . )	heap	pf	Heap[A] × Ref[A] → A with λ h, r. r ≠ null ∧ r ∈ h
. ( . := . )	heap	pf	Heap[A] × Ref[A] × A → Heap[A] with λ h, r, o. r ≠ null ∧ r ∈ h
. * .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. + .	nat-basic	f	Nat × Nat → Nat
. ++ .	set-basic	f	Set[A] × A → Set[A]
. ++ .	heap	pf	Heap[A] × Ref[A] → Heap[A] with λ h, r. r ≠ null ∧ ¬ r ∈ h
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -* .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. -- .	set-union	f	Set[A] × A → Set[A]
. -- .	heap	pf	Heap[A] × Ref[A] → Heap[A] with λ h, r. r ≠ null ∧ r ∈ h
. -> .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. -⊗ .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. < .	nat-basic	p	Nat × Nat
. > .	nat	p	Nat × Nat
. \ .	set-union	f	Set[A] × Set[A] → Set[A]
. \ .	heapfuns	f	Heap[A] × Set[Ref[A]] → Heap[A]
. \ .	heapfuns	f	Heap[A] × Heap[A] → Heap[A]
. ^*	relops	f	(A × A → Bool) → A × A → Bool
. ^-1	relops	f	(A × B → Bool) → B × A → Bool
. ∈ .	heap	p	Ref('A) × Heap('A)
. ∈ .	set-basic	p	'A × Set('A)
. ∩ .	set-union	f	Set[A] × Set[A] → Set[A]
. ∪ .	set-union	f	Set[A] × Set[A] → Set[A]
. ∪ .	heapfuns	f	Heap[A] × Heap[A] → Heap[A]
. ≡ .	heap-mod	f	Heap[A] × Heap[A] → Set[Ref[A]] → Bool
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('A) × Set('A)
. ⊆ .	heapfuns	p	Heap('A) × Heap('A)
. ⊆ .	heap-sep	p	(Heap('A) → Bool) × (Heap('A) → Bool)
. ⊗ .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. ⊥ .	heapfuns	p	Heap('A) × Heap('A)
. and .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. exists ( . )	set-union	p	Set('A) × ('A → Bool)
. filter ( . )	set-union	f	Set[A] × (A → Bool) → Set[A]
. forall ( . )	set-union	p	Set('A) × ('A → Bool)
. map ( . )	set-union	f	Set[A] × (A → B) → Set[B]
. o .	relops	f	(A × B → Bool) × (B × C → Bool) → A × C → Bool
. or .	heap-sep	f	(Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
. toFun	relops	pf	(A × B → Bool) → A → B with λ rel. λ a. funp(rel)
{ . }	set-union	f	A → Set[A]
{ . }	heap-sep	f	Heap[A] → Heap[A] → Bool
∅	heap	c	Heap[A]
∅	set-basic	c	Set[A]
⌜ . ⌝	heap-sep	f	Bool → Heap[A] → Bool
Heap	heap	s
Nat	nat-basic	s
Ref	polyref	s
Set	set-basic	s
alloc#	heap	pr	: Heap[A] → Ref[A] (nondeterministic)
cod .	relops	f	(A × B → Bool) → B → Bool
disjoint	set-union	p	Set('A) × Set('A)
dom .	relops	f	(A × B → Bool) → A → Bool
dom .	heapfuns	f	Heap[A] → Set[Ref[A]]
emp	heap-sep	p	Heap('A)
false	heap-sep	p	Heap('A)
footprint	heap-mod	p	Set(Ref('A)) × (Heap('A) → Bool) × Heap('A)
funp	relops	p	('A × 'B → Bool)
h	heap-mod	v	Heap[A]
hP	heap-mod	v	Heap[A] → Bool
inj	relops	p	('A × 'B → Bool)
ite	heap-sep	f	Bool × (Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] → Bool
modify	heap-mod	f	Set[Ref[A]] → Heap[A] × Heap[A] → Bool
modify*	heap-mod	f	Set[Ref[A]] → Heap[A] × Heap[A] → Bool
not .	heap-sep	f	(Heap[A] → Bool) → Heap[A] → Bool
null	polyref	c	Ref[A]
ob	heap-mod	v	A
pfunp	relops	p	('A × 'B → Bool)
precise	heap-sep	p	(Heap('A) → Bool)
r	heap-mod	v	Ref[A]
rs	heap-mod	v	Set[Ref[A]]
rtc	relops	f	Nat × (A × A → Bool) → A × A → Bool
surj	relops	p	('A × 'B → Bool)
total	relops	p	('A × 'B → Bool)
true	heap-sep	p	Heap('A)