[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
# .	nat-set	f	nat-set → nat
# .	avolume	f	avolume → 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
. + .	avolume	f	avolume × avolume → avolume
. ++ .	nat-set	f	nat-set × nat → nat-set
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	nat-set	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .butmax	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .butmin	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .data	aleb	pf	aleb → buffer with λ aleb. aleb.mapped?
. .data:= .	aleb	pf	aleb × buffer → aleb with λ aleb, buf. aleb.mapped?
. .mapped?	aleb	p	aleb
. .max	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .min	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	nat-set	p	nat-set × nat
. < .	nat-set	p	nat × nat-set
. > .	nat	p	nat × nat
. [ . ]	avolume	pf	avolume × nat × aleb → avolume with λ avol, n, aleb. n < # avol
. [ . ]	avolume	pf	avolume × nat → aleb with λ avol, n. n < # avol
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. \ .	nat-set	f	nat-set × nat-set → nat-set
. ∈ .	nat-set	p	nat × nat-set
. ∈ .	avolume	p	aleb × avolume
. ∈ .	buffer	p	data × buffer
. ∩ .	nat-set	f	nat-set × nat-set → nat-set
. ∪ .	nat-set	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	ebm-vol-inv	p	avolume × avolume
. ⊆ .	nat-set	p	nat-set × nat-set
{ . }	nat-set	f	nat → nat-set
∅	nat-set	c	nat-set
⌊ . ⌋	error-class	p	error
AVOL	ebm-avol-asm	v	avolume,flexible
BUF	ebm-avol-asm	v	buffer,flexible
BUF0	ebm-avol-asm	v	buffer,flexible
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
LNUM	ebm-avol-asm	v	nat,flexible
N	ebm-avol-asm	v	nat,flexible
N0	ebm-avol-asm	v	nat,flexible
N1	ebm-avol-asm	v	nat,flexible
OFFSET	ebm-avol-asm	v	nat,flexible
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
VOLSIZE	ebm-avol-asm	v	nat,flexible
aleb	aleb	s
aleb	aleb	v	aleb
aleb0	avolume	v	aleb
aleb1	avolume	v	aleb
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
avol	avolume	v	avolume
avol0	avolume	v	avolume
avol1	avolume	v	avolume
avol2	avolume	v	avolume
avolume	avolume	s
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	avolume	pp	avolume × aleb × nat × nat with λ avol, aleb, m, n. m + n ≤ # avol
cmp	avolume	pp	avolume × nat × avolume × nat × nat with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0
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	avolume	pf	avolume × nat × avolume × nat × nat → avolume with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
ebm-vol-inv	ebm-vol-inv	p	avolume
ebm_avol_change#	ebm-avol-asm	pr	nat × nat × buffer : avolume : error (nondeterministic)
ebm_avol_format#	ebm-avol-asm	pr	nat : : avolume × error (nondeterministic)
ebm_avol_get_leb_size#	ebm-avol-asm	pr	avolume : : nat
ebm_avol_get_page_size#	ebm-avol-asm	pr	avolume : : nat
ebm_avol_get_volume_size#	ebm-avol-asm	pr	avolume : : nat
ebm_avol_read#	ebm-avol-asm	pr	nat × nat × nat × nat × avolume : buffer : error (nondeterministic)
ebm_avol_recover#	ebm-avol-asm	pr	: avolume : error (nondeterministic)
ebm_avol_remap#	ebm-avol-asm	pr	nat : avolume : error (nondeterministic)
ebm_avol_sync_device#	ebm-avol-asm	pr	avolume : : error (nondeterministic)
ebm_avol_unmap#	ebm-avol-asm	pr	nat : avolume (nonfunctional)
ebm_avol_write#	ebm-avol-asm	pr	nat × nat × nat × nat × buffer : avolume : error (nondeterministic)
empty	buffer	c	data
empty	avolume	c	aleb
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
fail#	error-class	pr	: : error (nondeterministic)
fail_or_success#	error-class	pr	: : error (nondeterministic)
fill	avolume	pf	avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	avolume	f	avolume × aleb → avolume
id○	avolume	p	avolume × avolume × nat
id○	buffer	p	buffer × buffer × nat
idrange	avolume	pp	avolume × nat × nat with λ avol, m, n. m + n ≤ # avol
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
m	nat-basic	v	nat
m0	array-copy	v	nat
mapped	aleb	f	buffer → aleb
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkavolume	avolume	f	nat → avolume
mkbuf	buffer	f	nat → buffer
mkemparray	avolume	f	nat → avolume
mkempbuf	buffer	f	nat → buffer
mkzarray	avolume	f	nat → avolume
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	nat-set	v	nat
n3	nat-set	v	nat
n4	nat-set	v	nat
nat	nat-basic	s
nat-set	nat-set	s
ns	nat-set	v	nat-set
ns0	nat-set	v	nat-set
ns1	nat-set	v	nat-set
ns2	nat-set	v	nat-set
range=	avolume	p	avolume × nat × avolume × nat × nat
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
resize	avolume	f	avolume × nat → avolume
rev	avolume	pf	avolume × nat → avolume with λ avol, n. n ≤ # avol
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	avolume	f	avolume → avolume
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
splice	avolume	f	avolume × nat × avolume × nat × nat → avolume
subarray	avolume	pf	avolume × nat × nat → avolume with λ avol, m, n. m + n ≤ # avol
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
unmapped	aleb	c	aleb
zero	buffer	c	data
zero	avolume	c	aleb