路徑是路徑元素的清單，它表示到檔案、目錄或符號連結的路徑
路徑元素是非空的字串。有效字串的確切集合可能特定於某個檔案系統實作。
路徑元素不得在 {"", ".", "..", "/"} 中。
路徑元素不得包含字元 {'/', ':'}。
檔案系統可能有其他字串在路徑元素中不被允許。
驗證路徑元素時，當路徑無效時，應提出例外狀況 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
路徑 MAY 參考檔案系統中的目錄
isDir(FS, p): p in FS.Directories
目錄可能有子目錄，也就是說，檔案系統中可能存在其他路徑，其路徑以目錄開頭。只有目錄可能有子目錄。這可以用每個路徑的父目錄都必須是目錄來說明。
然後可以宣告路徑沒有父目錄，在這種情況下它是根目錄，或者它 MUST 有父目錄，而父目錄是目錄
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)}
路徑 MAY 參考檔案系統中包含資料的檔案；其路徑是資料字典中的金鑰
def isFile(FS, p) = p in FS.Files
路徑 MAY 參考符號連結
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) == {}
這表示只有檔案可以有資料。
此條件是不變的，且是所有操作 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(f))
未涵蓋：FileSystem 中的硬連結。如果 FileSystem 支援在 paths(FS) 中有多個參考指向相同的資料，則操作的結果未定義。
FileSystem 的此模型足以描述所有 FileSystem 查詢和操作，但排除元資料和權限操作。Hadoop FileSystem 和 FileContext 介面可以用查詢或變更 FileSystem 狀態的操作來指定。