[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
# .	buffer	f	buffer → nat
# .	abstract-volumes	f	abstract-volumes → nat
# .	abstract-volume	f	abstract-volume → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	abstract-volumes	f	abstract-volumes × volid → abstract-volumes
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .data	leb	pf	leb → buffer with λ leb. leb.mapped?
. .data:= .	leb	pf	leb × buffer → leb with λ leb, buf. leb.mapped?
. .fill	leb	pf	leb → nat with λ leb. leb.mapped?
. .fill:= .	leb	pf	leb × nat → leb with λ leb, m. leb.mapped?
. .mapped?	leb	p	leb
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	abstract-volumes	pf	abstract-volumes × volid → abstract-volume with λ avols, v. v ∈ avols
. [ . ]	abstract-volume	pf	abstract-volume × nat × leb → abstract-volume with λ evol, n, leb. n < # evol
. [ . ]	abstract-volume	pf	abstract-volume × nat → leb with λ evol, n. n < # evol
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	abstract-volumes	f	abstract-volumes × volid × abstract-volume → abstract-volumes
. ∈ .	abstract-volumes	p	volid × abstract-volumes
. ∈ .	abstract-volume	p	leb × abstract-volume
. ∈ .	buffer	p	data × buffer
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	ebm-base	p	abstract-volumes × abstract-volumes
. subseteq .	abstract-volumes	p	abstract-volumes × abstract-volumes
∅	abstract-volumes	c	abstract-volumes
⌊ . ⌋	error-class	p	error
EACCESS	error	c	error
EB_PAGE_SIZE	eraseblock	c	nat
EBADFD	error	c	error
ECOMMIT	error	c	error
EEXISTS	error	c	error
EFAIL	error	c	error
EINVAL	error	c	error
EIO	error	c	error
EISDIR	error	c	error
ENOENT	error	c	error
ENOMEM	error	c	error
ENOSPC	error	c	error
ENOTDIR	error	c	error
ENOTEMPTY	error	c	error
EROFS	error	c	error
ERR	error-class	v	error,flexible
ERR0	error-class	v	error,flexible
ESUCCESS	error	c	error
EUCLEAN	error	c	error
LEB_SIZE	eraseblock	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
abstract-volume	abstract-volume	s
abstract-volumes	abstract-volumes	s
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
avols	abstract-volumes	v	abstract-volumes
avols0	abstract-volumes	v	abstract-volumes
avols1	abstract-volumes	v	abstract-volumes
avols2	abstract-volumes	v	abstract-volumes
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	abstract-volume	pp	abstract-volume × leb × nat × nat with λ evol, leb, m, n. m + n ≤ # evol
cmp	abstract-volume	pp	abstract-volume × nat × abstract-volume × nat × nat with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	buffer	pf	buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	abstract-volume	pf	abstract-volume × nat × abstract-volume × nat × nat → abstract-volume with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
ebm-cons	ebm-base	p	abstract-volume
ebm-cons	ebm-base	p	abstract-volumes
ebm-initial	ebm-base	p	abstract-volumes
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
erased	leb	c	leb
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
evol	abstract-volume	v	abstract-volume
evol0	abstract-volume	v	abstract-volume
evol1	abstract-volume	v	abstract-volume
evol2	abstract-volume	v	abstract-volume
fail#	error-class	pr	: : error (nondeterministic)
fail_or_success#	error-class	pr	: : error (nondeterministic)
fill	buffer	f	buffer × data → buffer
fill	abstract-volume	pf	abstract-volume × leb × nat × nat → abstract-volume with λ evol, leb, n, m. n + m ≤ # evol
fill	abstract-volume	f	abstract-volume × leb → abstract-volume
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
id○	buffer	p	buffer × buffer × nat
id○	abstract-volume	p	abstract-volume × abstract-volume × nat
idrange	abstract-volume	pp	abstract-volume × nat × nat with λ evol, m, n. m + n ≤ # evol
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer × nat × nat
isempty	eraseblock	p	buffer
leb	leb	s
leb	leb	v	leb
leb0	abstract-volume	v	leb
leb1	abstract-volume	v	leb
m	nat-basic	v	nat
m0	array-copy	v	nat
mapped	leb	f	buffer × nat → leb
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkabstractvolume	abstract-volume	f	nat → abstract-volume
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	abstract-volume	pf	abstract-volume × nat → abstract-volume with λ evol, n. n ≤ # evol
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	abstract-volume	f	abstract-volume → abstract-volume
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	abstract-volume	pf	abstract-volume × nat × nat → abstract-volume with λ evol, m, n. m + n ≤ # evol
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
unmapped	leb	c	leb
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
valid-leb	ebm-base	p	leb
volid	volid	s
zero	buffer	c	data