[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
# .	laddress-list	f	laddress-list → nat
# .	avolume	f	avolume → nat
# .	list-data	f	list → nat
# .	string	f	string → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	laddress-list	f	laddress → laddress-list
. '	list	f	elem → list
. '	string	f	char → string
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	laddress-list	f	laddress-list × laddress → laddress-list
. + .	avolume	f	avolume × avolume → avolume
. + .	laddress-list	f	laddress-list × laddress-list → laddress-list
. + .	string	f	char × string → string
. + .	laddress-list	f	laddress × laddress-list → laddress-list
. + .	string	f	string × string → string
. + .	list	f	list × elem → list
. + .	string	f	string × char → string
. + .	list	f	list × list → list
. + .	list-data	f	elem × list → list
. ++ .	laddress-list	f	laddress-list × laddress → laddress-list
. ++ .	string	f	string × char → string
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	laddress-list	f	laddress × laddress → laddress-list
. +2 .	list	f	elem × elem → list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	laddress-list	f	laddress-list × laddress → laddress-list
. -1l .	list-del	f	list × elem → list
. -l .	string	f	string × char → string
. -l .	list-del	f	list × elem → list
. -l .	laddress-list	f	laddress-list × laddress → laddress-list
. -p .	laddress-list	f	laddress-list × nat → laddress-list
. -p .	string	f	string × nat → string
. -p .	list-del	f	list × nat → list
. .align↓	awbuf-inv	f	buffer → buffer
. .align↓	awbuf-inv	f	avolume → avolume
. .alignedsize	encoding-node-base	f	elem → nat
. .butlast	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .butlast	list-last	pf	list → list with λ x. x ≠ []
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .data	aleb	pf	aleb → buffer with λ aleb. aleb.mapped?
. .data:= .	aleb	pf	aleb × buffer → aleb with λ aleb, buf. aleb.mapped?
. .flashsize	encoding-node-base	f	elem → nat
. .flashsize	abs-list	f	list → nat
. .head	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .head	list-data	pf	list → elem with λ x. x ≠ []
. .isbuf?	bufleb	p	bufleb
. .ispadding	node-header	p	node-header
. .ispadding:= .	node-header	f	node-header × bool → node-header
. .last	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .last	list-last	pf	list → elem with λ x. x ≠ []
. .last	string	pf	string → char with λ str. str ≠ ""
. .leb	bufleb	pf	bufleb → nat with λ bleb. bleb.isbuf?
. .mapped?	aleb	p	aleb
. .off	laddress	f	laddress → nat
. .off:= .	laddress	f	laddress × nat → laddress
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	node-header	f	node-header → nat
. .size	laddress	f	laddress → nat
. .size:= .	node-header	f	node-header × nat → node-header
. .size:= .	laddress	f	laddress × nat → laddress
. .tail	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .tail	list-data	pf	list → list with λ x. x ≠ []
. .toString	debug	f	nat → string
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	laddress-list	p	laddress-list × laddress-list
. < .	list-data	p	list × list
. > .	nat	p	nat × nat
. [ . ]	laddress-list	pf	laddress-list × nat × laddress → laddress-list with λ lax, n, ladr. n < # lax
. [ . ]	laddress-list	pf	laddress-list × nat → laddress with λ lax, n. n < # lax
. [ . ]	list-del	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	list-del	pf	list × nat → elem with λ x, n. n < # x
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	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
. ↓ .	awbuf-inv	p	aleb × aleb
. ↓ .	awbuf-inv	p	avolume × avolume
. ∈ .	buffer	p	data × buffer
. ∈ .	laddress-list	p	laddress × laddress-list
. ∈ .	avolume	p	aleb × avolume
. ∈ .	list	p	elem × list
. ∈ .	string	p	char × string
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	laddress-list	p	laddress-list × laddress-list
. ⊑ .	string	p	string × string
. ⊑ .	list-last	p	list × list
. ⊒ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	string	p	string × string
. ⊒ .	list-last	p	list × list
@	laddress	f	nat × nat → laddress
[]	list-data	c	list
[]	laddress-list	c	laddress-list
⊏	string	p	string × string
⌊ . ⌋	error-class	p	error
ALIGNEDSIZE	encoding-node-base	v	nat,flexible
BUF	encoding-node-base	v	buffer,flexible
Boolvar	encoding-node-header	v	bool,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
ISPAD	encoding-node-base	v	bool,flexible
LEB_SIZE	eraseblock	c	nat
ND	encoding-node-base	v	elem,flexible
NDHD	encoding-node-base	v	node-header,flexible
NDSIZE	encoding-node-base	v	nat,flexible
NODE_HEADER_SIZE	node-header-size	c	nat
OFFSET	encoding-node-base	v	nat,flexible
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
SIZE	encoding-node-base	v	nat,flexible
SIZE0	encoding-node-base	v	nat,flexible
TRAILER	encoding-node-base	v	buffer,flexible
a	elem	v	elem
a0	list-data	v	elem
abs-failed	abs-node	p	buffer
abs-node	abs-node	p	buffer × elem
abs-nodes	abs-list	p	buffer × nat × list × laddress-list × bool
abs-nodes	abs-list	p	buffer × list × laddress-list × bool
abs-padding	abs-node	p	buffer
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
awbuf-inv	awbuf-inv	p	avolume × bufleb
b	elem	v	elem
bleb	bufleb	v	bufleb
boolvar	node-header	v	bool
boolvar0	node-header	v	bool
boolvar1	encoding-node-header	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
buffered	bufleb	f	nat → bufleb
bufleb	bufleb	s
butlastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
c	elem	v	elem
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
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
debug#	debug	pr	string :
decode_header#	encoding-node-header	pr	nat × buffer : node-header : error (nondeterministic)
decode_header_empty#	encoding-node-header	pr	nat × buffer : node-header × nat : error (nondeterministic)
decode_node#	encoding-node-base	pr	nat × nat × buffer : elem : error (nondeterministic)
decode_node_headerless#	encoding-node-headerless	pr	nat × buffer : elem × nat : error (nondeterministic)
disj	laddress-list	p	laddress-list × laddress-list
disj	string	p	string × string
disj	list-dup	p	list × list
dropn	list-prefixn	f	nat × list → list
dropn	laddress-list	f	nat × laddress-list → laddress-list
dups	laddress-list	p	laddress-list
dups	string	p	string
dups	list-dup	p	list
elem	elem	s
empty	buffer	c	data
empty	avolume	c	aleb
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
encode_header#	encoding-node-header	pr	node-header × nat : buffer : error (nondeterministic)
encode_header_empty#	encoding-node-header	pr	node-header × nat : buffer × nat : error (nondeterministic)
encode_node#	encoding-node-base	pr	elem × nat : nat × buffer : error (nondeterministic)
encode_node_headerless#	encoding-node-headerless	pr	elem × nat : buffer × nat : error (nondeterministic)
encoding-size	encoding-node-header	f	node-header → nat
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	buffer	f	buffer × data → buffer
fill	avolume	f	avolume × aleb → avolume
fill	avolume	pf	avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fillfirst	string	f	nat × char × string → string
fillfirst	laddress-list	f	nat × laddress × laddress-list → laddress-list
fillfirst	list-last	f	nat × elem × list → list
firstn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
frome	list-del	f	list × elem → list
frome	laddress-list	f	laddress-list × laddress → laddress-list
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
is-encoded	encoding	p	elem × buffer
is-encoded	encoding-node-header	p	node-header × buffer
is-encoded-empty	encoding-node-header	p	node-header × buffer
is-garbage	encoding	p	buffer
is-garbage-header	encoding-node-header	p	buffer
is-garbage-rnode-empty	encoding-node-header	p	buffer
isempty	eraseblock	p	buffer
isempty	eraseblock	p	buffer × nat × nat
ispad	encoding-node-base	v	bool
isvalidtrailer	node-header-size	p	buffer
laddress	laddress	s
laddress-list	laddress-list	s
ladr	laddress	v	laddress
ladr0	laddress-list	v	laddress
ladr1	laddress-list	v	laddress
ladr2	laddress-list	v	laddress
lastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
lastn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
lax	laddress-list	v	laddress-list
lax0	laddress-list	v	laddress-list
lax1	laddress-list	v	laddress-list
lax2	laddress-list	v	laddress-list
lax3	laddress-list	v	laddress-list
list	list-data	s
m	nat-basic	v	nat
m0	bufleb	v	nat
m1	laddress	v	nat
m2	laddress	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
mklist	laddress-list	f	laddress × nat → laddress-list
mklist	list-last	f	elem × nat → list
mklist	string	f	char × nat → string
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
nat	nat-basic	s
nd	encoding-node-headerless	v	elem
nd0	encoding-node-headerless	v	elem
nd1	encoding-node-headerless	v	elem
ndhd	node-header	v	node-header
ndhd0	encoding-node-header	v	node-header
ndhd1	encoding-node-header	v	node-header
nobuffer	bufleb	c	bufleb
node-header	node-header	s
node-size-headerless	encoding-node-headerless	f	elem → nat
nodeheader	node-header	f	nat × bool → node-header
pos	string	f	char × string → nat
pos	laddress-list	f	laddress × laddress-list → nat
pos	list-del	f	elem × list → nat
prefixn	laddress-list	f	nat × laddress-list → laddress-list
prefixn	list-prefixn	f	nat × list → list
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
restn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	buffer	f	buffer → buffer
rev	avolume	pf	avolume × nat → avolume with λ avol, n. n ≤ # avol
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	avolume	f	avolume → avolume
rev	laddress-list	f	laddress-list → laddress-list
rev	string	f	string → string
rev	list-last	f	list → list
rmdup	string	f	string → string
rmdup	laddress-list	f	laddress-list → laddress-list
rmdup	list-dup	f	list → list
slice	laddress-list	f	nat × nat × laddress-list → laddress-list
slice	list-prefixn	f	nat × nat × list → list
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
splice	avolume	f	avolume × nat × avolume × nat × nat → avolume
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
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
sublist	laddress-list	pf	nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax
sublist	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
synced	awbuf-inv	p	avolume
unmapped	aleb	c	aleb
validtrailer	node-header-size	c	buffer
weak	abs-list	v	bool
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
y	list-data	v	list
z	list-data	v	list
zero	buffer	c	data
zero	avolume	c	aleb