[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
# .	abstract-volume	f	abstract-volume → nat
# .	avolume	f	avolume → nat
# .	abstract-volumes	f	abstract-volumes → 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
. -- .	abstract-volumes	f	abstract-volumes × volid → abstract-volumes
. -- .	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	leb	pf	leb → buffer with λ leb. leb.mapped?
. .data	aleb	pf	aleb → buffer with λ aleb. aleb.mapped?
. .data:= .	aleb	pf	aleb × buffer → aleb with λ aleb, buf. aleb.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
. .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
. [ . ]	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
. [ . ]	abstract-volumes	f	abstract-volumes × volid × abstract-volume → abstract-volumes
. [ . ]	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
. ∈ .	abstract-volumes	p	volid × abstract-volumes
. ∈ .	abstract-volume	p	leb × abstract-volume
. ∩ .	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
. ⊆ .	ebm-base	p	abstract-volumes × abstract-volumes
. subseteq .	abstract-volumes	p	abstract-volumes × abstract-volumes
{ . }	nat-set	f	nat → nat-set
∅	abstract-volumes	c	abstract-volumes
∅	nat-set	c	nat-set
⌊ . ⌋	error-class	p	error
AVOL	ebm-avol-asm	v	avolume,flexible
AVOLS	ebm-asm	v	abstract-volumes,flexible
AVOLS0	ebm-asm	v	abstract-volumes,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
VOLID	ebm-asm	v	volid,flexible
VOLID0	ebm-asm	v	volid,flexible
VOLSIZE	ebm-avol-asm	v	nat,flexible
abs	ebm-vol-abs	f	leb → aleb
abs	ebm-vol-abs	f	abstract-volume → avolume
abstract-volume	abstract-volume	s
abstract-volumes	abstract-volumes	s
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
avols	abstract-volumes	v	abstract-volumes
avols0	abstract-volumes	v	abstract-volumes
avols1	abstract-volumes	v	abstract-volumes
avols2	abstract-volumes	v	abstract-volumes
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	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 × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
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
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
default-volid	default-volid	c	volid
ebm-cons	ebm-base	p	abstract-volume
ebm-cons	ebm-base	p	abstract-volumes
ebm-initial	ebm-base	p	abstract-volumes
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)
ebm_change#	ebm-asm	pr	volid × nat × nat × buffer : abstract-volumes : error (nondeterministic)
ebm_create_volume#	ebm-asm	pr	volid × nat : abstract-volumes : error (nondeterministic)
ebm_erase#	ebm-asm	pr	volid × nat : abstract-volumes : error (nondeterministic)
ebm_format#	ebm-asm	pr	: : abstract-volumes × error (nondeterministic)
ebm_get_leb_size#	ebm-asm	pr	abstract-volumes : : nat
ebm_get_page_size#	ebm-asm	pr	abstract-volumes : : nat
ebm_get_volume_size#	ebm-asm	pr	volid × abstract-volumes : : nat
ebm_map#	ebm-asm	pr	volid × nat : abstract-volumes : error (nondeterministic)
ebm_read#	ebm-asm	pr	volid × nat × nat × nat × nat × abstract-volumes : buffer : error (nondeterministic)
ebm_recover#	ebm-asm	pr	: abstract-volumes : error (nondeterministic)
ebm_sync_device#	ebm-asm	pr	abstract-volumes : : error (nondeterministic)
ebm_unmap#	ebm-asm	pr	volid × nat : abstract-volumes (nonfunctional)
ebm_vol_change#	ebm-vol-asm	pr	nat × nat × buffer × volid : abstract-volumes : error (nondeterministic)
ebm_vol_format#	ebm-vol-asm	pr	nat : volid × abstract-volumes : error (nondeterministic)
ebm_vol_get_leb_size#	ebm-vol-asm	pr	abstract-volumes : : nat
ebm_vol_get_page_size#	ebm-vol-asm	pr	abstract-volumes : : nat
ebm_vol_get_volume_size#	ebm-vol-asm	pr	volid × abstract-volumes : : nat
ebm_vol_read#	ebm-vol-asm	pr	nat × nat × nat × nat × volid × abstract-volumes : buffer : error (nondeterministic)
ebm_vol_recover#	ebm-vol-asm	pr	: abstract-volumes : volid × error (nondeterministic)
ebm_vol_remap#	ebm-vol-asm	pr	nat × volid : abstract-volumes : error (nondeterministic)
ebm_vol_sync_device#	ebm-vol-asm	pr	abstract-volumes : : error (nondeterministic)
ebm_vol_unmap#	ebm-vol-asm	pr	nat × volid : abstract-volumes (nonfunctional)
ebm_vol_write#	ebm-vol-asm	pr	nat × nat × nat × nat × buffer × volid : abstract-volumes : error (nondeterministic)
ebm_write#	ebm-asm	pr	volid × nat × nat × nat × nat × buffer : abstract-volumes : error (nondeterministic)
empty	buffer	c	data
empty	avolume	c	aleb
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	avolume	pf	avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol
fill	abstract-volume	f	abstract-volume × leb → abstract-volume
fill	abstract-volume	pf	abstract-volume × leb × nat × nat → abstract-volume with λ evol, leb, n, m. n + m ≤ # evol
fill	avolume	f	avolume × aleb → avolume
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
id○	buffer	p	buffer × buffer × nat
id○	avolume	p	avolume × avolume × nat
id○	abstract-volume	p	abstract-volume × abstract-volume × nat
idrange	avolume	pp	avolume × nat × nat with λ avol, m, n. m + n ≤ # avol
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
mapped	aleb	f	buffer → aleb
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkabstractvolume	abstract-volume	f	nat → abstract-volume
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	abstract-volume	pf	abstract-volume × nat → abstract-volume with λ evol, n. n ≤ # evol
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	abstract-volume	f	abstract-volume → abstract-volume
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	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
unmapped	aleb	c	aleb
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	avolume	c	aleb
zero	buffer	c	data