路径是路径元素的列表，表示到文件、目录或符号链接的路径
路径元素是非空字符串。有效字符串的确切集合可能特定于特定的文件系统实现。
路径元素不得在 {"", ".", "..", "/"} 中。
路径元素不得包含字符 {'/', ':'}。
文件系统可能还有其他不允许在路径元素中出现的字符串。
在验证路径元素时，当路径无效时，应引发异常 InvalidPathException [HDFS]
valid-path-element(List[String]): bool如果路径元素 pe 中的任何字符都在禁止字符集中，或者元素整体无效，则该元素无效
forall e in pe: not (e in {'/', ':'})
not pe in {"", ".", "..", "/"}
valid-path(List[PathElement]): bool如果路径 p 中的所有路径元素都有效，则该路径是有效的
def valid-path(path): forall pe in path: valid-path-element(pe)
所有可能路径的集合是Paths；这是所有有效路径元素列表的无限集合。
由空列表表示的路径 [] 是根路径，并由字符串 "/" 表示。
parent(path:Path): Path部分函数 parent(path:Path):Path 提供父路径，可以使用列表切片来定义。
def parent(pe) : pe[0:-1]
先决条件
path != []
filename(Path): PathElement路径中的最后一个路径元素称为文件名。
def filename(p) : p[-1]
先决条件
p != []
childElements(Path p, Path q): Path部分函数 childElements:(Path p, Path q):Path 是 p 中紧跟路径 q 的路径元素列表。
def childElements(p, q): p[len(q):]
先决条件
# The path 'q' must be at the head of the path 'p' q == p[:len(q)]
ancestors(Path): List[Path]所有路径的列表，这些路径要么是路径 p 的直接父路径，要么是 p 的祖先的父路径。
此定义处理绝对路径，但不处理相对路径；它需要重新处理，以便根元素是显式的，大概通过声明根（并且仅根）路径元素可以是 [‘/’]。
然后，相对路径可以与绝对路径区分开来，作为任何函数的输入，并在双参数函数（例如 rename）中的第二个条目解析。
文件系统 FS 包含一组目录、一个路径字典和一个符号链接字典。
(Directories:Set[Path], Files:[Path:List[byte]], Symlinks:Set[Path])
访问器函数返回文件系统的特定元素。
def FS.Directories = FS.Directories def files(FS) = FS.Files def symlinks(FS) = FS.Symlinks def filenames(FS) = keys(FS.Files)
整个路径集是所有可能路径的有限子集，以及将路径解析为数据、目录谓词或符号链接的函数。
def paths(FS) = FS.Directories + filenames(FS) + FS.Symlinks)
如果路径在此聚合集中，则认为该路径存在。
def exists(FS, p) = p in paths(FS)
根路径“/”是一个由路径 [“/”] 表示的目录，它必须始终存在于文件系统中。
def isRoot(p) = p == ["/"]. forall FS in FileSystems : ["/"] in FS.Directories
路径可能引用文件系统中的目录。
isDir(FS, p): p in FS.Directories
目录可能具有子目录，即，文件系统中可能存在其他路径，其路径以目录开头。只有目录可以具有子目录。这可以通过说每个路径的父路径必须是目录来表示。
然后可以声明路径没有父路径，在这种情况下它是根目录，或者它必须有一个父路径，该父路径是目录。
forall p in paths(FS) : isRoot(p) or isDir(FS, parent(p))
由于所有目录的父目录本身必须满足此标准，因此隐式地只有叶节点可以是文件或符号链接。
此外，由于每个文件系统都包含根路径，因此每个文件系统都必须至少包含一个目录。
目录可以具有子目录。
def children(FS, p) = {q for q in paths(FS) where parent(q) == p}
子路径中没有重复名称，因为所有路径都取自路径元素列表的集合。集合中不能有重复条目，因此没有具有重复名称的子项。
路径D是路径P的后代，如果它是路径P的直接子项或祖先是路径P的直接子项
def isDescendant(P, D) = parent(D) == P where isDescendant(P, parent(D))
目录 P 的后代是文件系统中所有路径，其路径以路径 P 开头 - 即它们的父级是 P 或祖先是 P
def descendants(FS, D) = {p for p in paths(FS) where isDescendant(D, p)}
路径可以引用文件系统中具有数据的某个文件；其路径是数据字典中的一个键
def isFile(FS, p) = p in FS.Files
路径可以引用符号链接
def isSymlink(FS, p) = p in symlinks(FS)
文件系统 FS 中路径 p 的长度是存储的数据的长度，如果它是目录，则长度为 0
def length(FS, p) = if isFile(p) : return length(data(FS, p)) else return 0
用户的主目录是文件系统的一个隐式部分，它派生自使用文件系统的进程的用户 ID
def getHomeDirectory(FS) : Path
函数 getHomeDirectory 返回文件系统和当前用户帐户的主目录。对于某些文件系统，路径为 ["/","users", System.getProperty("user-name")]。但是，对于 HDFS，用户名是从用于对客户端进行 HDFS 身份验证的凭据派生的。这可能与本地用户帐户名称不同。
路径不能同时引用文件、目录或符号链接
FS.Directories ^ keys(data(FS)) == {}
FS.Directories ^ symlinks(FS) == {}
keys(data(FS))(FS) ^ symlinks(FS) == {}
这意味着只有文件可以具有数据。
此条件是不变的，并且是操作文件系统 FS 状态的所有操作的隐式后置条件。
如果文件位于加密区中，则数据将被加密。
def inEncryptionZone(FS, path): bool
加密的性质和创建加密区的机制是本规范未涵盖的实现细节。不保证加密的质量。元数据未加密。
加密区中目录下的所有文件和目录也位于加密区中。
forall d in directories(FS): inEncyptionZone(FS, d) implies
forall c in children(FS, d) where (isFile(FS, c) or isDir(FS, c)) :
inEncyptionZone(FS, c)
对于加密区中的所有文件，数据都已加密，但未定义加密类型和规范。
forall f in files(FS) where inEncyptionZone(FS, f): isEncrypted(data(f))
未涵盖：文件系统中的硬链接。如果文件系统支持paths(FS)中的多个引用指向相同的数据，则操作的结果是未定义的。
此文件系统模型足以描述所有文件系统查询和操作，但不包括元数据和权限操作。Hadoop FileSystem和FileContext接口可以根据查询或更改文件系统状态的操作来指定。