パスとは、ファイル、ディレクトリ、またはシンボリックリンクへのパスを表すパス要素のリストです。
パス要素は空でない文字列です。有効な文字列の正確なセットは、特定のファイルシステム実装に固有のものである場合があります。
パス要素は{"", ".", "..", "/"}に含まれていてはなりません。
パス要素には、文字{'/', ':'}が含まれていてはなりません。
ファイルシステムには、パス要素で許可されていない他の文字列が存在する場合があります。
パス要素を検証する場合、パスが無効な場合は例外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)
すべての可能なパスのセットは*パス*です。これは、有効なパス要素のすべてのリストの無限集合です。
空のリスト[]で表されるパスは、*ルートパス*であり、文字列"/"で表されます。
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は、パスqの後に続くp内のパス要素のリストです。
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`などの2つの引数を取る関数の2番目のエントリで解決できます。
ファイルシステム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))
すべてのディレクトリの親ディレクトリ自体がこの基準を満たす必要があるため、リーフノードのみがファイルまたはシンボリックリンクである可能性があることは暗黙的です。
さらに、すべてのファイルシステムにはルートパスが含まれているため、すべてのファイルシステムには少なくとも1つのディレクトリが含まれている必要があります。
ディレクトリには子がいる場合があります。
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
暗号化の性質と暗号化ゾーンを作成するためのメカニズムは、この仕様では coveredれていない実装の詳細です。暗号化の品質については保証されません。メタデータは暗号化されません.
暗号化ゾーン内のディレクトリの下にあるすべてのファイルとディレクトリも暗号化ゾーンにあります.
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))
対象外：ファイルシステム内のハードリンク。ファイルシステムが*パス（FS）*内の複数の参照が同じデータを指すことをサポートしている場合、操作の結果は未定義です。
このファイルシステムモデルは、メタデータおよびパーミッション操作を除く、すべてのファイルシステムクエリと操作を記述するのに十分です。HadoopのFileSystemおよびFileContextインターフェースは、ファイルシステムの状態を照会または変更する操作として指定できます。