[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
# .	vtbl	f	vtbl → nat
. * .	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
. -- .	vtbl	f	vtbl × volid → vtbl
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	vtbl	pf	vtbl × volid → nat with λ vtbl, v. v ∈ vtbl
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	vtbl	f	vtbl × volid × nat → vtbl
. ∈ .	vtbl	p	volid × vtbl
. ∈ .	buffer	p	data × buffer
. ∪ .	vtbl	f	vtbl × vtbl → vtbl
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	vtbl	p	vtbl × vtbl
. ⊥ .	vtbl	p	vtbl × vtbl
∅	vtbl	c	vtbl
⌊ . ⌋	error-class	p	error
BUF	encoding-vtbl	v	buffer,flexible
Boolvar	encoding-nat	v	bool,flexible
EACCESS	error	c	error
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
ENCODED_NAT_SIZE	encoding-nat	c	nat
ENCODED_VOLID_SIZE	encoding-volid	c	nat
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
INDEX	encoding-vtbl	v	nat,flexible
M	encoding-vtbl	v	nat,flexible
N	encoding-vtbl	v	nat,flexible
SIZE	encoding-vtbl	v	nat,flexible
VOLID	encoding-vtbl	v	volid,flexible
VTBL	encoding-vtbl	v	vtbl,flexible
boolvar	encoding-nat	v	bool
boolvar0	encoding-nat	v	bool
boolvar1	encoding-nat	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
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
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
decode_nat#	encoding-nat	pr	nat × buffer : nat × nat : error (nondeterministic)
decode_volid#	encoding-volid	pr	nat × buffer : volid × nat : error (nondeterministic)
decode_vtbl#	encoding-vtbl	pr	buffer : : vtbl × error (nondeterministic)
empty	buffer	c	data
encode_nat#	encoding-nat	pr	nat × nat : buffer × nat : error (nondeterministic)
encode_volid#	encoding-volid	pr	volid × nat : buffer × nat : error (nondeterministic)
encode_vtbl#	encoding-vtbl	pr	: vtbl × buffer : error (nondeterministic)
encoding-size	encoding-nat	f	nat → nat
encoding-size	encoding-volid	f	volid → 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	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
is-encoded	encoding-nat	p	nat × buffer
is-encoded	encoding-volid	p	volid × buffer
is-encoded	encoding-vtbl	p	vtbl × buffer
is-encoded-rec	encoding-vtbl	p	vtbl × buffer
is-garbage-nat	encoding-nat	p	buffer
is-garbage-volid	encoding-volid	p	buffer
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
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
n2	vtbl	v	nat
n3	vtbl	v	nat
n4	vtbl	v	nat
n5	vtbl	v	nat
nat	nat-basic	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
volid	volid	s
vtbl	vtbl	s
vtbl	vtbl	v	vtbl
vtbl0	vtbl	v	vtbl
vtbl1	vtbl	v	vtbl
vtbl2	vtbl	v	vtbl
zero	buffer	c	data