[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
# .	open-file-handles	f	nat-set → nat
# .	open-file-handles	f	open-file-handles → nat
# .	buffer	f	buffer → nat
# .	fidbag	f	fidbag → nat
# .	file-data-store	f	file-data-store → nat
# .	file-data-store	f	fidset → nat
# .	path	f	path → nat
# .	directory-tree-inst	f	stringset → nat
# .	directory-tree-base	f	entries-tree → nat
# .	string	f	string → nat
#n .	directory-tree	f	entries-tree → nat
#n .	directory-tree	f	directory-tree → nat
. '	string	f	char → string
. '	path	f	string → path
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	path	f	path × string → path
. + .	string	f	char × string → string
. + .	path	f	path × path → path
. + .	string	f	string × string → string
. + .	path	f	string × path → path
. + .	string	f	string × char → string
. ++ .	open-file-handles	f	nat-set × nat → nat-set
. ++ .	file-data-store	f	fidset × fid → fidset
. ++ .	fidbag	f	fidbag × fid → fidbag
. ++ .	directory-tree-inst	f	stringset × string → stringset
. ++ .	path	f	path × string → path
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	path	f	string × string → path
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	file-data-store	f	file-data-store × fid → file-data-store
. -- .	file-data-store	f	fidset × fid → fidset
. -- .	open-file-handles	f	nat-set × nat → nat-set
. -- .	directory-tree-inst	f	stringset × string → stringset
. -- .	open-file-handles	f	open-file-handles × nat → open-file-handles
. -- .	directory-tree-base	f	entries-tree × string → entries-tree
. -- .	fidbag	f	fidbag × fid → fidbag
. -- .	directory-tree	f	directory-tree × path → directory-tree
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	path	f	path × string → path
. -1l .	string	f	string × char → string
. -l .	string	f	string × char → string
. -l .	path	f	path × string → path
. -p .	path	f	path × nat → path
. -p .	string	f	string × nat → string
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .content	file-data	f	file-data → buffer
. .content:= .	file-data	f	file-data × buffer → file-data
. .dir?	directory-tree	p	directory-tree
. .directory	inode	p	inode
. .directory:= .	inode	f	inode × bool → inode
. .entries	directory-tree	f	directory-tree → entries-tree
. .entries:= .	directory-tree	f	directory-tree × entries-tree → directory-tree
. .fid	directory-tree	f	directory-tree → fid
. .fid	file-handle	f	file-handle → fid
. .fid:= .	directory-tree	f	directory-tree × fid → directory-tree
. .fid:= .	file-handle	f	file-handle × fid → file-handle
. .fids	posix-base	f	open-file-handles → fidset
. .fids	directory-tree-fids	f	directory-tree → fidbag
. .fids	directory-tree-fids	f	entries-tree → fidbag
. .head	path	pf	path → string with λ p. p ≠ ε
. .ino	inode	f	inode → nat
. .ino:= .	inode	f	inode × nat → inode
. .last	path	pf	path → string with λ p. p ≠ ε
. .last	string	pf	string → char with λ str. str ≠ ""
. .meta	file-data	f	file-data → metadata
. .meta	inode	f	inode → metadata
. .meta	directory-tree	f	directory-tree → metadata
. .meta:= .	file-data	f	file-data × metadata → file-data
. .meta:= .	directory-tree	f	directory-tree × metadata → directory-tree
. .meta:= .	inode	f	inode × metadata → inode
. .mode	file-handle	f	file-handle → file-mode
. .mode:= .	file-handle	f	file-handle × file-mode → file-handle
. .nlink	inode	f	inode → nat
. .nlink:= .	inode	f	inode × nat → inode
. .nsubdirs	inode	f	inode → nat
. .nsubdirs:= .	inode	f	inode × nat → inode
. .pos	file-handle	f	file-handle → nat
. .pos:= .	file-handle	f	file-handle × nat → file-handle
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	inode	f	inode → nat
. .size:= .	inode	f	inode × nat → inode
. .subdirs	directory-tree	f	directory-tree → stringset
. .tail	path	pf	path → path with λ p. p ≠ ε
. < .	nat-basic	p	nat × nat
. < .	path	p	path × path
. > .	nat	p	nat × nat
. [ . ]	open-file-handles	pf	open-file-handles × nat → file-handle with λ ofh, fd. fd ∈ ofh
. [ . ]	path	pf	path × nat × string → path with λ p, n, str. n < # p
. [ . ]	path	pf	path × nat → string with λ p, n. n < # p
. [ . ]	file-data-store	f	file-data-store × fid × file-data → file-data-store
. [ . ]	directory-tree-base	pf	entries-tree × string → directory-tree with λ sdt, str. str ∈ sdt
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	file-data-store	pf	file-data-store × fid → file-data with λ fs, fid. fid ∈ fs
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	directory-tree-base	f	entries-tree × string × directory-tree → entries-tree
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	directory-tree	f	directory-tree × path → directory-tree
. [ . ]	open-file-handles	f	open-file-handles × nat × file-handle → open-file-handles
. [ . ]	directory-tree	f	directory-tree × path × directory-tree → directory-tree
. \ .	file-data-store	f	fidset × fidset → fidset
. \ .	file-data-store	f	file-data-store × fidset → file-data-store
. \ .	directory-tree-inst	f	stringset × stringset → stringset
. \ .	open-file-handles	f	open-file-handles × nat-set → open-file-handles
. \ .	directory-tree-inst	f	entries-tree × stringset → entries-tree
. \ .	open-file-handles	f	nat-set × nat-set → nat-set
. \ .	fidbag	f	fidbag × fidbag → fidbag
. \| .	open-file-handles	f	open-file-handles × nat-set → open-file-handles
. \| .	file-data-store	f	file-data-store × fidset → file-data-store
. \| .	directory-tree-inst	f	entries-tree × stringset → entries-tree
. × .	directory-tree-base	f	string × directory-tree → stringdirectorytree
. ∈ .	open-file-handles	p	file-handle × open-file-handles
. ∈ .	buffer	p	data × buffer
. ∈ .	open-file-handles	p	nat × nat-set
. ∈ .	file-data-store	p	fid × file-data-store
. ∈ .	open-file-handles	p	nat × open-file-handles
. ∈ .	file-data-store	p	fid × fidset
. ∈ .	fidbag	p	fid × fidbag
. ∈ .	file-data-store	p	file-data × file-data-store
. ∈ .	directory-tree	p	path × directory-tree
. ∈ .	directory-tree-inst	p	string × stringset
. ∈ .	path	p	string × path
. ∈ .	directory-tree-inst	p	directory-tree × entries-tree
. ∈ .	directory-tree-base	p	stringdirectorytree × entries-tree
. ∈ .	string	p	char × string
. ∈ .	directory-tree-base	p	string × entries-tree
. ∩ .	file-data-store	f	fidset × fidset → fidset
. ∩ .	open-file-handles	f	nat-set × nat-set → nat-set
. ∩ .	directory-tree-inst	f	stringset × stringset → stringset
. ∪ .	file-data-store	f	fidset × fidset → fidset
. ∪ .	directory-tree-inst	f	stringset × stringset → stringset
. ∪ .	fidbag	f	fidbag × fidbag → fidbag
. ∪ .	open-file-handles	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	open-file-handles	p	nat-set × nat-set
. ⊆ .	open-file-handles	p	open-file-handles × open-file-handles
. ⊆ .	file-data-store	p	file-data-store × file-data-store
. ⊆ .	fidbag	p	fidbag × fidbag
. ⊆ .	file-data-store	p	fidset × fidset
. ⊆ .	directory-tree-inst	p	stringset × stringset
. ⊆ .	directory-tree-base	p	entries-tree × entries-tree
. ⊑ .	path	p	path × path
. ⊑ .	string	p	string × string
. ⊒ .	path	p	path × path
. ⊒ .	string	p	string × string
. ⊕ .	file-data-store	f	file-data-store × file-data-store → file-data-store
. ⊕ .	open-file-handles	f	open-file-handles × open-file-handles → open-file-handles
. ⊕ .	directory-tree-inst	f	entries-tree × entries-tree → entries-tree
{ . }	file-data-store	f	fid → fidset
{ . }	open-file-handles	f	nat → nat-set
{ . }	directory-tree-inst	f	string → stringset
{ . }	fidbag	f	fid → fidbag
ε	path	c	path
∅	file-data-store	c	file-data-store
∅	file-data-store	c	fidset
∅	directory-tree-inst	c	stringset
∅	directory-tree-base	c	entries-tree
∅	fidbag	c	fidbag
∅	open-file-handles	c	open-file-handles
∅	open-file-handles	c	nat-set
⊏	string	p	string × string
⌊ . ⌋	error-class	p	error
Boolvar	directory-tree-inst	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
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
MODE_R	file-mode	c	file-mode
MODE_RW	file-mode	c	file-mode
MODE_W	file-mode	c	file-mode
Pentries-tree	directory-tree-inst	v	entries-tree → bool
Ptree	directory-tree	v	directory-tree → bool
SEEK_CUR	seekflag	c	seekflag
SEEK_END	seekflag	c	seekflag
SEEK_SET	seekflag	c	seekflag
boolvar	inode	v	bool
boolvar0	inode	v	bool
boolvar1	directory-tree-inst	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	path	pf	nat × path → path with λ n, p. n ≤ # p
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
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
count	fidbag	f	fid × fidbag → nat
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
datasyncp	posix-pre	v	bool
directory-tree	directory-tree-base	s
disj	path	p	path × path
disj	string	p	string × string
dnode	directory-tree-base	f	metadata × entries-tree → directory-tree
dom .	file-data-store	f	file-data-store → fidset
dom .	open-file-handles	f	open-file-handles → nat-set
dom .	directory-tree-inst	f	entries-tree → stringset
dups	path	p	path
dups	string	p	string
empty	buffer	c	data
entries-tree	directory-tree-base	s
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
f	file-data	v	file-data
f0	file-data-store	v	file-data
f1	file-data-store	v	file-data
f2	file-data-store	v	file-data
fail#	error-class	pr	: : error (nondeterministic)
fail_or_success#	error-class	pr	: : error (nondeterministic)
fd	open-file-handles	v	nat
fd1	open-file-handles	v	nat
fd2	open-file-handles	v	nat
fh	file-handle	v	file-handle
fh0	open-file-handles	v	file-handle
fh1	open-file-handles	v	file-handle
fh2	open-file-handles	v	file-handle
fid	file-id	s
fid	file-id	v	fid
fid0	fidbag	v	fid
fid1	file-data-store	v	fid
fid2	file-data-store	v	fid
fidb	fidbag	v	fidbag
fidb0	fidbag	v	fidbag
fidb1	fidbag	v	fidbag
fidb2	fidbag	v	fidbag
fidbag	fidbag	s
fids	file-data-store	v	fidset
fids-cons	posix-base	p	directory-tree × file-data-store × open-file-handles
fids0	file-data-store	v	fidset
fids1	file-data-store	v	fidset
fids2	file-data-store	v	fidset
fidset	file-data-store	s
file-data	file-data	s
file-data-store	file-data-store	s
file-handle	file-handle	s
file-mode	file-mode	s
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
fillfirst	path	f	nat × string × path → path
fillfirst	string	f	nat × char × string → string
firstn	path	pf	nat × path → path with λ n, p. n ≤ # p
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
fnode	directory-tree-base	f	fid → directory-tree
frome	string	f	string × char → string
frome	path	f	path × string → path
fs	file-data-store	v	file-data-store
fs0	file-data-store	v	file-data-store
fs1	file-data-store	v	file-data-store
fs2	file-data-store	v	file-data-store
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
inode	inode	s
inode	inode	v	inode
lastn	path	pf	nat × path → path with λ n, p. n ≤ # p
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	inode	v	nat
m1	inode	v	nat
m2	inode	v	nat
m3	inode	v	nat
m4	inode	v	nat
m5	inode	v	nat
m6	inode	v	nat
max	min-max	f	nat × nat → nat
max	open-file-handles-ext	f	open-file-handles → nat
md	metadata	v	metadata
md0	inode	v	metadata
meta	posix-base	f	path × directory-tree × file-data-store → metadata
metadata	metadata	s
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mkfh	file-handle	f	fid × file-mode × nat → file-handle
mkfile	file-data	f	metadata × buffer → file-data
mkinode	inode	f	nat × metadata × bool × nat × nat × nat → inode
mklist	string	f	char × nat → string
mkpath	path	f	string × nat → path
mkzbuf	buffer	f	nat → buffer
mode	file-mode	v	file-mode
mode0	file-handle	v	file-mode
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
nat-set	open-file-handles	s
nats	open-file-handles	v	nat-set
nats0	open-file-handles	v	nat-set
nats1	open-file-handles	v	nat-set
nats2	open-file-handles	v	nat-set
ofh	open-file-handles	v	open-file-handles
ofh0	open-file-handles	v	open-file-handles
ofh1	open-file-handles	v	open-file-handles
ofh2	open-file-handles	v	open-file-handles
open-file-handles	open-file-handles	s
p	path	v	path
p'	path	v	path
p0	path	v	path
p1	path	v	path
parent	path	pf	path → path with λ p. p ≠ ε
path	path	s
path	posix-base	v	path
path'	posix-base	v	path
pos	string	f	char × string → nat
pos	path	f	string × path → nat
posix-crash	posix-base	p	directory-tree × file-data-store × open-file-handles × directory-tree × file-data-store × open-file-handles
pr	posix-permission	p	user × path × directory-tree × file-data-store
pr	permission	p	user × metadata
pre-close	posix-pre	p	nat × error × user × directory-tree × file-data-store × open-file-handles
pre-create	posix-pre	p	path × metadata × error × user × directory-tree × file-data-store × open-file-handles
pre-fsync	posix-pre	p	path × bool × error × user × directory-tree × file-data-store × open-file-handles
pre-link	posix-pre	p	path × path × error × user × directory-tree × file-data-store × open-file-handles
pre-mkdir	posix-pre	p	path × metadata × error × user × directory-tree × file-data-store × open-file-handles
pre-open	posix-pre	p	path × file-mode × error × user × directory-tree × file-data-store × open-file-handles
pre-read	posix-pre	p	nat × nat × error × user × directory-tree × file-data-store × open-file-handles
pre-readdir	posix-pre	p	path × error × user × directory-tree × file-data-store × open-file-handles
pre-readmeta	posix-pre	p	path × error × user × directory-tree × file-data-store × open-file-handles
pre-renam	posix-pre	p	path × path × error × user × directory-tree × file-data-store × open-file-handles
pre-rmdir	posix-pre	p	path × error × user × directory-tree × file-data-store × open-file-handles
pre-seek	posix-pre	p	nat × nat × seekflag × error × user × directory-tree × file-data-store × open-file-handles
pre-truncate	posix-pre	p	path × nat × error × user × directory-tree × file-data-store × open-file-handles
pre-unlink	posix-pre	p	path × error × user × directory-tree × file-data-store × open-file-handles
pre-write	posix-pre	p	nat × buffer × nat × error × user × directory-tree × file-data-store × open-file-handles
pre-writemeta	posix-pre	p	path × metadata × error × user × directory-tree × file-data-store × open-file-handles
pw	posix-permission	p	user × path × directory-tree × file-data-store
pw	permission	p	user × metadata
px	posix-permission	p	user × path × directory-tree × file-data-store
px	permission	p	user × metadata
px-parent	posix-permission	p	user × path × directory-tree × file-data-store
py	posix-permission	p	user × path × directory-tree × file-data-store
q	path	v	path
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	path	pf	nat × path → path with λ n, p. n ≤ # p
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
rev	path	f	path → path
rev	string	f	string → string
rmdup	string	f	string → string
rmdup	path	f	path → path
root	posix-base	v	directory-tree
sdt	directory-tree-base	v	entries-tree
sdt0	directory-tree-base	v	entries-tree
sdt1	directory-tree-base	v	entries-tree
sdt2	directory-tree-base	v	entries-tree
seekflag	seekflag	s
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
str	string	v	string
str-tree	directory-tree-base	v	stringdirectorytree
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
stringdirectorytree	directory-tree-base	s
strings	directory-tree-inst	v	stringset
strings0	directory-tree-inst	v	stringset
strings1	directory-tree-inst	v	stringset
strings2	directory-tree-inst	v	stringset
stringset	directory-tree-inst	s
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
sublist	path	pf	nat × nat × path → path with λ n, m, p. n + m ≤ # p
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
tree	directory-tree-base	v	directory-tree
tree0	directory-tree-base	v	directory-tree
tree1	directory-tree-base	v	directory-tree
tree2	directory-tree-base	v	directory-tree
user	user	s
user	user	v	user
whence	seekflag	v	seekflag
zero	buffer	c	data