路径是由一系列路径元素组成的列表，表示指向文件、目录或符号链接的路径
路径元素是非空字符串。有效字符串的具体集合可能特定于某个特定的FileSystem实现。
路径元素不能包含在 {"", ".", "..", "/"} 中。
路径元素不能包含字符 {'/', ':'}。
文件系统可能包含其他不允许出现在路径元素中的字符串。
在验证路径元素时，当路径无效时应抛出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:Map[Path:List[byte]], Symlinks:Map[Path:Path])
访问器函数返回文件系统的特定元素
def directories(FS) = FS.Directories def files(FS) = FS.Files def symlinks(FS) = keys(FS.Symlinks) def filenames(FS) = keys(FS.Files)
整个路径集合是所有可能路径的有限子集，以及用于将路径解析为数据、目录谓词或符号链接的函数：
def paths(FS) = FS.Directories + filenames(FS) + symlinks(FS)
如果路径存在于这个聚合集合中，则认为该路径存在：
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 的直接子路径，则称路径 D 是路径 P 的后代路径：
def isDescendant(P, D) = parent(D) == P or 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 keys(FS.Files)
路径可能引用符号链接：
def isSymlink(FS, p) = p in symlinks(FS)
文件存储数据：
def data(FS, p) = files(FS)[p]
文件系统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进行身份验证的凭据，这可能与本地用户账户名不同。
路径不能同时引用文件、目录或符号链接中的多个
directories(FS) ^ filenames(FS) == {}
directories(FS) ^ symlinks(FS) == {}
filenames(FS) ^ symlinks(FS) == {}
这意味着只有文件可以包含数据。
此条件是恒定的，并且是所有操作操作FileSystem 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(FS, f))
未涵盖：文件系统中的硬链接。如果文件系统支持在路径(FS)中存在多个引用指向同一数据，则操作结果将未定义。
这种文件系统模型足以描述所有文件系统查询和操作（不包括元数据和权限操作）。Hadoop的FileSystem和FileContext接口可以通过查询或更改文件系统状态的操作来定义。