[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	buffer	function, buffer → nat
#	pebs	function, pebs → nat
#	array	function, array → nat
%	nat-div	partial function, nat × nat → nat
*	nat-mult	function, nat × nat → nat
+	buffer	function, buffer × buffer → buffer
+	array-splice	function, array × array → array
+	nat-basic	function, nat × nat → nat
+1	nat-basic	function, nat → nat
-	nat	partial function, nat × nat → nat
-1	nat-basic	partial function, nat → nat
.bad	peb	predicate, peb
.bad:=	peb	function, peb × bool → peb
.data	peb	function, peb → buffer
.data:=	peb	function, peb × buffer → peb
.fill	peb	function, peb → nat
.fill:=	peb	function, peb × nat → peb
/	nat-div	partial function, nat × nat → nat
<	nat-basic	predicate, nat × nat
>	nat	predicate, nat × nat
BITFLIPS	mtd-asm	variable, bool,flexible
BUF	mtd-asm	variable, buffer,flexible
BUF0	mtd-asm	variable, buffer,flexible
EACCESS	error	constant, error
EBADFD	error	constant, error
EB_PAGE_SIZE	eraseblock	constant, nat
ECOMMIT	error	constant, error
EEXISTS	error	constant, error
EFAIL	error	constant, error
EINVAL	error	constant, error
EIO	error	constant, error
EISDIR	error	constant, error
ENOENT	error	constant, error
ENOMEM	error	constant, error
ENOSPC	error	constant, error
ENOTDIR	error	constant, error
ENOTEMPTY	error	constant, error
EROFS	error	constant, error
ERR	error-class	variable, error,flexible
ERR0	error-class	variable, error,flexible
ESUCCESS	error	constant, error
EUCLEAN	error	constant, error
ISBAD	mtd-asm	variable, bool,flexible
LEB_SIZE	eraseblock	constant, nat
N	mtd-asm	variable, nat,flexible
N0	mtd-asm	variable, nat,flexible
N1	mtd-asm	variable, nat,flexible
OFFSET	mtd-asm	variable, nat,flexible
PAGES_PER_LEB	eraseblock	constant, nat
PAGES_PER_PEB	eraseblock	constant, nat
PEB	mtd-asm	variable, peb,flexible
PEBS	mtd-asm	variable, pebs,flexible
PEB_SIZE	eraseblock	constant, nat
PNUM	mtd-asm	variable, nat,flexible
PNUM0	mtd-asm	variable, nat,flexible
]	buffer	partial function, buffer × nat × data → buffer
]	buffer	partial function, buffer × nat → data
]	pebs	partial function, pebs × nat × peb → pebs
]	pebs	partial function, pebs × nat → peb
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
a	elem	variable, elem
align↑	align	function, nat × nat → nat
align↓	align	function, nat × nat → nat
ar	array	variable, array
ar0	array	variable, array
ar1	array	variable, array
ar2	array	variable, array
array	array	sort,
b	elem	variable, elem
bitflips	mtd-asm	variable, bool
bool	bool	sort,
boolvar	bool	variable, bool
boolvar0	bool	variable, bool
buf	buffer	variable, buffer
buf0	buffer	variable, buffer
buf1	buffer	variable, buffer
buf2	buffer	variable, buffer
buffer	buffer	sort,
c	elem	variable, elem
cmp	buffer	partial predicate, buffer × data × nat × nat
cmp	buffer	partial predicate, buffer × nat × buffer × nat × nat
cmp	pebs	partial predicate, pebs × peb × nat × nat
cmp	pebs	partial predicate, pebs × nat × pebs × nat × nat
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
copy	buffer	partial function, buffer × nat × buffer × nat × nat → buffer
copy	pebs	partial function, pebs × nat × pebs × nat × nat → pebs
copy	array-copy	partial function, array × nat × array × nat × nat → array
d	data	variable, data
d0	data	variable, data
d1	data	variable, data
d2	data	variable, data
data	data	sort,
elem	elem	sort,
empty	buffer	constant, data
empty	array-splice	constant, elem
emptyleb	eraseblock	constant, buffer
emptypage	eraseblock	constant, buffer
emptypeb	eraseblock	constant, buffer
err	error	variable, error
err0	error	variable, error
err1	error	variable, error
error	error	sort,
fail#	error-class	procedure, : : error
fail_or_success#	error-class	procedure, : : error
fill	buffer	partial function, buffer × data × nat × nat → buffer
fill	buffer	function, buffer × data → buffer
fill	pebs	partial function, pebs × peb × nat × nat → pebs
fill	pebs	function, pebs × peb → pebs
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
idrange	buffer	partial predicate, buffer × nat × nat
idrange	pebs	partial predicate, pebs × nat × nat
idrange	array-copy	partial predicate, array × nat × nat
id○	buffer	predicate, buffer × buffer × nat
id○	pebs	predicate, pebs × pebs × nat
id○	array-copy	predicate, array × array × nat
is-aligned	align	predicate, nat × nat
isbad	mtd-asm	variable, bool
isempty	eraseblock	predicate, buffer × nat × nat
isempty	eraseblock	predicate, buffer
m	nat-basic	variable, nat
m0	array-copy	variable, nat
m1	mtd-base	variable, nat
m2	mtd-base	variable, nat
max	min-max	function, nat × nat → nat
min	min-max	function, nat × nat → nat
mkarray	array	function, nat → array
mkbuf	buffer	function, nat → buffer
mkemparray	array-splice	function, nat → array
mkempbuf	buffer	function, nat → buffer
mkpeb	peb	function, buffer × nat × bool → peb
mkpebs	pebs	function, nat → pebs
mkzarray	array-splice	function, nat → array
mkzbuf	buffer	function, nat → buffer
mtd-cons	mtd-base	predicate, pebs
mtd-valid-peb	mtd-base	predicate, peb
mtd_asm_erase#	mtd-asm	procedure, nat : pebs : error
mtd_asm_get_blockcount#	mtd-asm	procedure, pebs : : nat
mtd_asm_get_page_size#	mtd-asm	procedure, pebs : : nat
mtd_asm_get_peb_size#	mtd-asm	procedure, pebs : : nat
mtd_asm_init#	mtd-asm	procedure, : : pebs × error
mtd_asm_isbad#	mtd-asm	procedure, nat × pebs : : bool × error
mtd_asm_markbad#	mtd-asm	procedure, nat : pebs : error
mtd_asm_read#	mtd-asm	procedure, nat × nat × nat × nat × pebs : buffer : bool × error
mtd_asm_write#	mtd-asm	procedure, nat × nat × nat × nat × buffer : pebs : error
n	nat-basic	variable, nat
n0	nat-basic	variable, nat
n1	nat-basic	variable, nat
nat	nat-basic	sort,
peb	peb	variable, peb
peb	peb	sort,
peb0	pebs	variable, peb
peb1	pebs	variable, peb
pebs	pebs	variable, pebs
pebs	pebs	sort,
pebs0	pebs	variable, pebs
pebs1	pebs	variable, pebs
pebs2	pebs	variable, pebs
range=	buffer	predicate, buffer × nat × buffer × nat × nat
range=	array-splice	predicate, array × nat × array × nat × nat
resize	buffer	function, buffer × nat → buffer
resize	array-splice	function, array × nat → array
rev	buffer	partial function, buffer × nat → buffer
rev	buffer	function, buffer → buffer
rev	pebs	partial function, pebs × nat → pebs
rev	pebs	function, pebs → pebs
rev	array-copy	partial function, array × nat → array
rev	array-copy	function, array → array
splice	buffer	function, buffer × nat × buffer × nat × nat → buffer
splice	array-splice	function, array × nat × array × nat × nat → array
subarray	buffer	partial function, buffer × nat × nat → buffer
subarray	pebs	partial function, pebs × nat × nat → pebs
subarray	array-copy	partial function, array × nat × nat → array
zero	buffer	constant, data
zero	array-splice	constant, elem
∈	buffer	predicate, data × buffer
∈	pebs	predicate, peb × pebs
∈	array-copy	predicate, elem × array
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⌋	error-class	predicate, error