類別 org.apache.hadoop.fs.FileSystem

前置條件

if not exists(FS, p) : raise FileNotFoundException

後置條件

result = stat: FileStatus where:
    if isFile(FS, p) :
        stat.length = len(FS.Files[p])
        stat.isdir = False
        stat.blockSize > 0
    elif isDir(FS, p) :
        stat.length = 0
        stat.isdir = True
    elif isSymlink(FS, p) :
        stat.length = 0
        stat.isdir = False
        stat.symlink = FS.Symlinks[p]
    stat.hasAcl = hasACL(FS, p)
    stat.isEncrypted = inEncryptionZone(FS, p)
    stat.isErasureCoded = isErasureCoded(FS, p)

傳回的路徑 FileStatus 狀態另外載有 ACL、加密和刪除編碼資訊的詳細資料。可以查詢 getFileStatus(Path p).hasAcl() 以找出路徑是否有 ACL。可以查詢 getFileStatus(Path p).isEncrypted() 以找出路徑是否已加密。getFileStatus(Path p).isErasureCoded() 會告訴路徑是否已刪除編碼。

YARN 的分散式快取讓應用程式透過 Job.addCacheFile() 和 Job.addCacheArchive() 將路徑新增到容器和應用程式中快取。快取會將新增為應用程式間可共用的世界可讀取資源路徑，並以不同的方式下載它們，除非它們宣告為已加密。

為了避免容器啟動期間的失敗，特別是在使用委派權杖時，未實作檔案和目錄的 POSIX 存取權限的檔案系統和物件儲存庫，必須始終傳回 true 給 isEncrypted() 謂詞。這可以在建立 FileStatus 執行個體時，將 encrypted 旗標設定為 true 來完成。

前置條件

後置條件

此呼叫會在呼叫時內部記錄元資料服務的狀態。這可確保從任何元資料複本進行後續讀取的一致性。它確保用戶端絕不會存取記錄狀態之前的元資料狀態。

HDFS 實作注意事項

HDFS 在 HA 模式下透過呼叫 Active NameNode 並要求其最新的日誌交易 ID 來支援 msync()。更多詳細資料請參閱 HDFS 文件 從 HDFS Observer NameNode 進行一致讀取

前置條件

後置條件

result = p where valid-path(FS, p)

在呼叫方法時，不需要路徑存在，或者如果存在，則不需要指向目錄。然而，程式碼傾向於假設 not isFile(FS, getHomeDirectory()) 成立，以致於後續程式碼可能會失敗。

實作注意事項

• FTPFileSystem 會從遠端檔案系統查詢此值，如果發生連線問題，可能會失敗並傳回 RuntimeException 或其子類別。執行作業的時間沒有限制。

前置條件

路徑 path 必須存在

if not exists(FS, path) : raise FileNotFoundException

後置條件

if isFile(FS, path) and filter.accept(path) :
  result = [ getFileStatus(path) ]

elif isFile(FS, path) and not filter.accept(P) :
  result = []

elif isDir(FS, path):
  result = [
    getFileStatus(c) for c in children(FS, path) if filter.accepts(c)
  ]

隱含不變式：透過 listStatus() 擷取的子項目的 FileStatus 內容等於對相同路徑呼叫 getFileStatus() 的內容

forall fs in listStatus(path) :
  fs == getFileStatus(fs.path)

結果排序：沒有保證列出項目會排序。雖然 HDFS 目前會傳回字母數字排序的清單，但 Posix readdir() 和 Java 的 File.listFiles() API 呼叫都沒有定義傳回值的任何排序。需要對結果進行統一排序順序的應用程式必須自行執行排序。

Null 傳回：3.0.0 之前的本機檔案系統會在存取錯誤時傳回 null。這被視為錯誤。預期在存取錯誤時會傳回 IOException。

原子性和一致性

當 listStatus() 作業傳回呼叫者時，並不能保證回應中所包含的資訊為最新。詳細資訊可能會過時，包括任何目錄的內容、任何檔案的屬性，以及所提供路徑的存在。

目錄的狀態可能會在評估過程中變更。

• 在路徑 P 中建立一個條目後，且在對檔案系統進行任何其他變更之前，listStatus(P) 必須找到檔案並傳回其狀態。

• 在路徑 P 中刪除一個條目後，且在對檔案系統進行任何其他變更之前，listStatus(P) 必須引發 FileNotFoundException。

• 在路徑 P 中建立一個條目後，且在對檔案系統進行任何其他變更之前，listStatus(parent(P)) 的結果應該包含 getFileStatus(P) 的值。

• 在路徑 P 中建立一個條目後，且在對檔案系統進行任何其他變更之前，listStatus(parent(P)) 的結果不應該包含 getFileStatus(P) 的值。

這並非理論上的可能性，當目錄包含數千個檔案時，在 HDFS 中可以觀察到這一點。

考慮一個目錄 "/d"，其內容為

a
part-0000001
part-0000002
...
part-9999999

如果檔案數量多到 HDFS 在每個回應中傳回部分清單，則如果清單 listStatus("/d") 與作業 rename("/d/a","/d/z")) 同時執行，結果可能是

[a, part-0000001, ... , part-9999999]
[part-0000001, ... , part-9999999, z]
[a, part-0000001, ... , part-9999999, z]
[part-0000001, ... , part-9999999]

雖然這種情況不太可能發生，但可能會發生。在 HDFS 中，只有在列出具有許多子目錄的目錄時，才可能會出現這些不一致的檢視。

其他檔案系統可能具有更強的一致性保證，或更輕易地傳回不一致的資料。

前置條件

所有路徑都必須存在。無需唯一性。

forall p in paths :
  exists(fs, p) else raise FileNotFoundException

後置條件

結果是一個陣列，其條目包含路徑清單中找到的每個狀態元素，且沒有其他元素。

result = [listStatus(p, filter) for p in paths]

實作可能會合併重複的條目；和/或透過辨識重複的路徑並只列出條目一次來最佳化作業。

預設實作會遍歷清單；它不會執行任何最佳化。

原子性和一致性約束與 listStatus(Path, PathFilter) 相同。

前置條件

路徑 path 必須存在

exists(FS, path) : raise FileNotFoundException

後置條件

操作會產生一組結果，resultset，等於 listStatus(path, filter) 的結果

if isFile(FS, path) and filter.accept(path) :
  resultset =  [ getLocatedFileStatus(FS, path) ]

elif isFile(FS, path) and not filter.accept(path) :
  resultset = []

elif isDir(FS, path) :
  resultset = [
    getLocatedFileStatus(FS, c)
     for c in children(FS, path) where filter.accept(c)
  ]

操作 getLocatedFileStatus(FS, path: Path): LocatedFileStatus 定義為 LocatedFileStatus 執行個體 ls 的產生器，其中

fileStatus = getFileStatus(FS, path)

bl = getFileBlockLocations(FS, path, 0, fileStatus.len)

locatedFileStatus = new LocatedFileStatus(fileStatus, bl)

反覆運算器中傳回 resultset 元素的順序未定義。

原子性和一致性約束與 listStatus(Path, PathFilter) 相同。

前置條件

exists(FS, path) else raise FileNotFoundException

前置條件

exists(FS, path) else raise FileNotFoundException

後置條件

傳回 ContentSummary 物件，其中包含提供路徑的目錄計數和檔案計數等資訊。

原子性和一致性約束與 listStatus(Path, PathFilter) 相同。

前置條件

if s < 0 or l < 0 : raise {HadoopIllegalArgumentException, InvalidArgumentException}

• HDFS 會為無效的偏移量或長度擲回 HadoopIllegalArgumentException；這會延伸 IllegalArgumentException。

後置條件

如果檔案系統具有位置感知，它必須傳回區塊位置清單，其中可以找到範圍 [s:s+l] 中的資料。

if f == null :
    result = null
elif f.getLen() <= s:
    result = []
else result = [ locations(FS, b) for b in blocks(FS, p, s, s+l)]

其中

  def locations(FS, b) = a list of all locations of a block in the filesystem

  def blocks(FS, p, s, s +  l)  = a list of the blocks containing data(FS, path)[s:s+l]

請注意，由於 length(FS, f) 定義為 0（如果 isDir(FS, f)），因此在目錄上執行 getFileBlockLocations() 的結果為 []

如果檔案系統沒有位置感知，它應該傳回

  [
    BlockLocation(["localhost:9866"] ,
              ["localhost"],
              ["/default/localhost"]
               0, f.getLen())
   ] ;

*Hadoop 1.0.3 中的錯誤表示必須提供與叢集拓撲相同元素數量的拓撲路徑，因此檔案系統應該傳回 "/default/localhost" 路徑。雖然這不再是問題，但通常會保留此慣例。

前置條件

if p == null : raise NullPointerException
if not exists(FS, p) : raise FileNotFoundException

後置條件

result = getFileBlockLocations(getFileStatus(FS, P), S, L)

前置條件

後置條件

result = integer > 0

雖然此結果沒有定義的最小值，因為它用於在提交工作期間分割工作，但過小的區塊大小會導致分割不佳的工作負載，甚至會導致 JobSubmissionClient 和等效的記憶體用盡，因為它會計算分割區。

任何實際上不會將檔案分割成區塊的 FileSystem 都應傳回一個數字，以進行有效率的處理。FileSystem 可以讓使用者進行設定（物件儲存器連接器通常會這樣做）。

前置條件

後置條件

result = integer  >= 0

此操作的結果通常與 getDefaultBlockSize() 相同，不會檢查給定路徑是否存在。

支援掛載點的檔案系統可能對不同的路徑有不同的預設值，在這種情況下，應傳回目標路徑的特定預設值。

如果路徑不存在，這不是錯誤：必須傳回檔案系統該部分的預設/建議值。

前置條件

if not exists(FS, p) :  raise FileNotFoundException

後置條件

if len(FS, P) > 0:  getFileStatus(P).getBlockSize() > 0
result == getFileStatus(P).getBlockSize()

1. 此操作的結果必須與 getFileStatus(P).getBlockSize() 的值相同。
2. 根據推論，對於長度大於 0 的任何檔案，它必須大於 0。

前置條件

路徑必須是目錄或不存在

 if exists(FS, p) and not isDir(FS, p) :
     raise [ParentNotDirectoryException, FileAlreadyExistsException, IOException]

沒有祖先可以是檔案

forall d = ancestors(FS, p) : 
    if exists(FS, d) and not isDir(FS, d) :
        raise [ParentNotDirectoryException, FileAlreadyExistsException, IOException]

後置條件

FS' where FS'.Directories' = FS.Directories + [p] + ancestors(FS, p)
result = True

檔案系統的目錄、檔案和符號連結的條件排他性需求必須成立。

探測路徑和目錄建立的存在和類型必須是原子性的。包含 `mkdirs(parent(F))` 的複合操作可以是原子性的。

回傳值總是為 true，即使沒有建立新的目錄（這在 HDFS 中有定義）。

前置條件

對於不覆寫建立，檔案不能存在

if not overwrite and isFile(FS, p)  : raise FileAlreadyExistsException

寫入或覆寫目錄必須失敗。

if isDir(FS, p) : raise {FileAlreadyExistsException, FileNotFoundException, IOException}

沒有祖先可以是檔案

forall d = ancestors(FS, p) : 
    if exists(FS, d) and not isDir(FS, d) :
        raise [ParentNotDirectoryException, FileAlreadyExistsException, IOException]

檔案系統可能會因為其他原因拒絕要求，例如檔案系統為唯讀（HDFS）、區塊大小低於允許的最小值（HDFS）、複製計數超出範圍（HDFS）、超過名稱空間或檔案系統的配額、保留名稱等。所有拒絕都應該為 `IOException` 或其子類別，並且可以是 `RuntimeException` 或其子類別。例如，HDFS 可能會引發 `InvalidPathException`。

後置條件

FS' where :
   FS'.Files'[p] == []
   ancestors(p) is-subset-of FS'.Directories'

result = FSDataOutputStream

在指定的路徑末端必須存在一個零位元組檔案，所有人都看得見。

更新的（有效）檔案系統必須包含路徑的所有父目錄，由 `mkdirs(parent(p))` 建立。

結果是 `FSDataOutputStream`，它可能透過其操作產生新的檔案系統狀態，其中包含 `FS.Files[p]` 的更新值

已回傳串流的行為在 輸出 中說明。

實作注意事項

• 有些實作會將建立拆分為檢查檔案是否存在和實際建立。這表示操作不是原子性的：如果檔案在兩個測試之間由另一個用戶端建立，則使用 `overwrite==true` 建立檔案的用戶端可能會失敗。

• S3A 和其他潛在的物件儲存體連接器目前不會變更 `FS` 狀態，直到輸出串流 `close()` 操作完成。這是物件儲存體和檔案系統行為之間的重大差異，因為它允許 >1 個用戶端使用 `overwrite=false` 建立檔案，並可能混淆檔案/目錄邏輯。特別是，在使用物件儲存體時，使用 `create()` 取得檔案的獨佔鎖定（沒有錯誤建立檔案的人員會被視為鎖定的持有者）可能不是安全的演算法。

• 物件儲存體可能會在建立檔案時建立一個空檔案作為標記。但是，具有 `overwrite=true` 語意的物件儲存體可能無法原子性地實作這一點，因此無法使用 `overwrite=false` 建立檔案作為程序之間的隱式排除機制。

• 嘗試在目錄上建立檔案時，本機檔案系統會引發 `FileNotFoundException`，因此它會列為此前提條件失敗時可能會引發的例外狀況。

• 未涵蓋：符號連結。符號連結的已解析路徑會用作 `create()` 操作的最後路徑引數

實作注意事項

createFile(p) 只會傳回一個 FSDataOutputStreamBuilder，而且不會立即對檔案系統進行變更。當在 FSDataOutputStreamBuilder 上呼叫 build() 時，會驗證建立器的參數，並在底層檔案系統上呼叫 create(Path p)。build() 具有與 create(Path p) 相同的先決條件和後置條件。

• 與 create(Path p) 類似，檔案預設會被覆寫，除非指定 builder.overwrite(false)。
• 與 create(Path p) 不同，預設不會建立遺失的父目錄，除非指定 builder.recursive()。

前置條件

if not exists(FS, p) : raise FileNotFoundException

if not isFile(FS, p) : raise [FileAlreadyExistsException, FileNotFoundException, IOException]

後置條件

FS' = FS
result = FSDataOutputStream

傳回值：FSDataOutputStream，它可以透過將資料附加到現有清單來更新項目 FS.Files[p]。

已回傳串流的行為在 輸出 中說明。

實作注意事項

appendFile(p) 只會傳回一個 FSDataOutputStreamBuilder，而且不會立即對檔案系統進行變更。當在 FSDataOutputStreamBuilder 上呼叫 build() 時，會驗證建立器的參數，並在底層檔案系統上呼叫 append()。build() 具有與 append() 相同的先決條件和後置條件。

前置條件

if not isFile(FS, p)) : raise [FileNotFoundException, IOException]

這是一個重要的先決條件。某些檔案系統的實作（例如物件儲存）可以透過延後其 HTTP GET 作業，直到傳回的 FSDataInputStream 上的第一次 read()，來縮短一輪往返時間。然而，許多客戶端程式碼確實依賴於在 open() 作業時執行存在的檢查。實作必須在建立時檢查檔案是否存在。這並不表示檔案及其資料在後續的 read() 或任何後繼作業時仍然存在。

後置條件

result = FSDataInputStream(0, FS.Files[p])

結果提供對 FS.Files[p] 定義的位元組陣列的存取；無論該存取是在呼叫 open() 作業時對內容的存取，或是在 FS 的後續狀態中是否以及如何擷取該資料的變更，這都是實作細節。

結果必須對操作的本地和遠端呼叫者相同。

HDFS 實作注意事項

1. 嘗試穿越符號連結時，HDFS 可能會拋出 UnresolvedPathException

2. 如果路徑存在於元資料中，但找不到任何其區塊的拷貝，HDFS 會拋出 IOException("無法開啟檔案名稱 " + src)；-FileNotFoundException 看起來會更準確且有用。

前置條件

let stat = getFileStatus(Path p)
let FS' where:
  (FS.Directories', FS.Files', FS.Symlinks')
  p' in paths(FS') where:
    exists(FS, stat.path) implies exists(FS', p')

在解析時，FileStatus 實例的參照與 getPathHandle(FileStatus) 的結果相同。PathHandle 可用於後續操作，以確保呼叫之間的不變性。

options 參數指定後續呼叫（例如 open(PathHandle)）是否會在參照資料或位置變更時成功。預設情況下，任何修改都會導致錯誤。呼叫者可以指定放寬，即使參照存在於不同的路徑和/或其資料已變更，也能讓操作成功。

如果實作無法支援呼叫者指定的語意，則必須拋出 UnsupportedOperationException。預設選項集如下。

不需變更所有權、延伸屬性和其他元資料以符合 PathHandle。實作可以自訂限制條件來延伸 HandleOpt 參數集。

後置條件

result = PathHandle(p')

實作注意事項

PathHandle 的參照對象是在建立 FileStatus 執行個體時的名稱空間，而非建立 PathHandle 時的狀態。實作 MAY 拒絕建立或解析有效但服務成本昂貴的 PathHandle 執行個體。

實作透過複製物件進行重新命名的物件儲存體，除非已解析物件的譜系，否則不可宣稱支援 CONTENT 和 REFERENCE。

必須可以序列化 PathHandle 執行個體，並在一個或多個處理序、另一部機器上重新建立執行個體，且在未來的任意時間點上重新建立，而不會變更其語意。如果實作無法再保證其不變性，則必須拒絕解析執行個體。

HDFS 實作注意事項

HDFS 不支援 PathHandle 對目錄或符號連結的參照。對 CONTENT 和 REFERENCE 的支援會透過 INode 查詢檔案。INode 在 NameNode 中並非唯一，因此聯合叢集應在 PathHandle 中包含足夠的元資料，以偵測來自其他名稱空間的參照。

前置條件

let fd = getPathHandle(FileStatus stat)
if stat.isdir : raise IOException
let FS' where:
  (FS.Directories', FS.Files', FS.Symlinks')
  p' in FS.Files' where:
    FS.Files'[p'] = fd
if not exists(FS', p') : raise InvalidPathHandleException

實作必須依照 getPathHandle(FileStatus) 在建立時指定的約束，解析 PathHandle 的參照對象。

FileSystem 滿足此合約所需的元資料 MAY 編碼在 PathHandle 中。

後置條件

result = FSDataInputStream(0, FS.Files'[p'])

傳回的串流會受到 open(Path) 傳回串流的約束限制。在開啟時檢查的約束 MAY 會對串流有效，但並非保證如此。

例如，使用 CONTENT 約束建立的 PathHandle MAY 傳回一個在開啟後會忽略檔案更新的串流，如果在解析 open(PathHandle) 時檔案未修改。

實作注意事項

實作 MAY 在伺服器或在將串流傳回給用戶端之前檢查不變性。例如，實作可能會開啟檔案，然後使用 getFileStatus(Path) 驗證 PathHandle 中的不變性，以實作 CONTENT。這可能會產生假陽性，且需要額外的 RPC 流量。

前置條件

具有子目錄且 recursive == False 的目錄無法刪除

if isDir(FS, p) and not recursive and (children(FS, p) != {}) : raise IOException

（HDFS 在這裡引發 PathIsNotEmptyDirectoryException。）

後置條件

if not exists(FS, p):
    FS' = FS
    result = False

if isFile(FS, p) :
    FS' = (FS.Directories, FS.Files - [p], FS.Symlinks)
    result = True

if isRoot(p) and children(FS, p) == {} :
    FS ' = FS
    result = (undetermined)

if isDir(FS, p) and not isRoot(p) and children(FS, p) == {} :
    FS' = (FS.Directories - [p], FS.Files, FS.Symlinks)
    result = True

原子性

• 刪除檔案必須是原子動作。

• 刪除空目錄必須是原子動作。

• 目錄樹的遞迴刪除必須是原子動作。

實作注意事項

• 物件儲存體和其他非傳統檔案系統（模擬目錄樹的檔案系統）傾向於將 delete() 實作為遞迴列示和逐項刪除操作。這可能會破壞用戶端應用程式對 O(1) 原子目錄刪除的預期，讓儲存體無法作為 HDFS 的替代方案。

前置條件

在計算出最終 dest 路徑後，必須對目標路徑執行所有檢查。

來源 src 必須存在

exists(FS, src) else raise FileNotFoundException

dest 不能是 src 的子項

if isDescendant(FS, src, dest) : raise IOException

這隱含涵蓋了 isRoot(FS, src) 的特殊情況。

dest 必須是根，或具有存在的父項

isRoot(FS, dest) or exists(FS, parent(dest)) else raise IOException

目標的父路徑不能是檔案

if isFile(FS, parent(dest)) : raise IOException

這隱含涵蓋了父項的所有祖先。

目標路徑的結尾處不能有現有檔案

if isFile(FS, dest) : raise FileAlreadyExistsException, IOException

後置條件

if isDir(FS, src) and src == dest :
    FS' = FS
    result = (undefined)

 if isFile(FS, src) and src == dest :
     FS' = FS
     result = True

if isFile(FS, src) and src != dest:
    FS' where:
        not exists(FS', src)
        and exists(FS', dest)
        and data(FS', dest) == data (FS, source)
    result = True

if isDir(FS, src) and isDir(FS, dest) and src != dest :
    FS' where:
        not exists(FS', src)
        and dest in FS'.Directories
        and forall c in descendants(FS, src) :
            not exists(FS', c))
        and forall c in descendants(FS, src) where isDir(FS, c):
            isDir(FS', dest + childElements(src, c)
        and forall c in descendants(FS, src) where not isDir(FS, c):
                data(FS', dest + childElements(s, c)) == data(FS, c)
    result = True

  not exists(FS, parent(dest))

FS' = FS; result = False

exists(FS', parent(dest))

FS' = FS
result = false

前置條件

if not exists(FS, p) : raise FileNotFoundException

if sources==[] : raise IllegalArgumentException

所有來源都必須在同一個目錄中

for s in sources: if parent(S) != parent(p) raise IllegalArgumentException

所有區塊大小都必須與目標相符

for s in sources: getBlockSize(FS, S) == getBlockSize(FS, p)

沒有重複路徑

not (exists p1, p2 in (sources + [p]) where p1 == p2)

HDFS：除了最後一個檔案之外的所有來源檔案都必須是完整區塊

for s in (sources[0:length(sources)-1] + [p]):
  (length(FS, s) mod getBlockSize(FS, p)) == 0

後置條件

FS' where:
 (data(FS', T) = data(FS, T) + data(FS, sources[0]) + ... + data(FS, srcs[length(srcs)-1]))
 and for s in srcs: not exists(FS', S)

HDFS 的限制可能是透過變更 inode 參考來實作 concat 的實作細節，將它們串聯在一起。由於 Hadoop 核心程式碼庫中沒有其他檔案系統實作這個方法，因此無法區分實作細節和規格。

前置條件

if not exists(FS, p) : raise FileNotFoundException

if isDir(FS, p) : raise [FileNotFoundException, IOException]

if newLength < 0 || newLength > len(FS.Files[p]) : raise HadoopIllegalArgumentException

HDFS：來源檔案必須關閉。無法對開啟用於寫入或附加的檔案執行縮減。

後置條件

FS' where:
    len(FS.Files[p]) = newLength

傳回：如果縮減已完成且檔案可以立即開啟用於附加，則傳回 true，否則傳回 false。

HDFS：HDFS 傳回 false 以表示已啟動調整最後一個區塊長度的背景程序，且客戶端應等到它完成才能繼續進行進一步的檔案更新。

並行性

如果在執行 truncate() 時開啟輸入串流，則與正在縮減的檔案部分相關的讀取作業結果未定義。

前置條件

來源和目的地必須不同

if src = dest : raise FileExistsException

目的地和來源不能彼此為後代

if isDescendant(src, dest) or isDescendant(dest, src) : raise IOException

來源檔案或目錄必須存在於本機

if not exists(LocalFS, src) : raise FileNotFoundException

目錄無法複製到檔案中，不論覆寫旗標設定為何

if isDir(LocalFS, src) and isFile(FS, dst) : raise PathExistsException

對於所有情況，除了上述前提條件會引發例外情況的情況之外，如果目的地存在，則必須將覆寫旗標設定為 TRUE，作業才能成功。這也會覆寫目的地中的所有檔案/目錄

if exists(FS, dst) and not overwrite : raise PathExistsException

決定複製的最終名稱

假設來源 base 上有一個基本路徑和一個子路徑 child，其中 base 位於 ancestors(child) + child 中

def final_name(base, child, dest):
    is base = child:
        return dest
    else:
        return dest + childElements(base, child)

來源為檔案的結果 isFile(LocalFS, src)

對於檔案，目的地中的資料會變成來源中的資料。所有祖先都是目錄。

if isFile(LocalFS, src) and (not exists(FS, dest) or (exists(FS, dest) and overwrite)):
    FS' = FS where:
        FS'.Files[dest] = LocalFS.Files[src]
        FS'.Directories = FS.Directories + ancestors(FS, dest)
    LocalFS' = LocalFS where
        not delSrc or (delSrc = true and delete(LocalFS, src, false))
else if isFile(LocalFS, src) and isDir(FS, dest):
    FS' = FS where:
        let d = final_name(src, dest)
        FS'.Files[d] = LocalFS.Files[src]
    LocalFS' = LocalFS where:
        not delSrc or (delSrc = true and delete(LocalFS, src, false))

對於本機 LocalFS 和遠端 FS，沒有預期檔案變更會是原子性的。

來源為目錄的結果 isDir(LocalFS, src)

if isDir(LocalFS, src) and (isFile(FS, dest) or isFile(FS, dest + childElements(src))):
    raise FileAlreadyExistsException
else if isDir(LocalFS, src):
    if exists(FS, dest):
        dest' = dest + childElements(src)
        if exists(FS, dest') and not overwrite:
            raise PathExistsException
    else:
        dest' = dest

    FS' = FS where:
        forall c in descendants(LocalFS, src):
            not exists(FS', final_name(c)) or overwrite
        and forall c in descendants(LocalFS, src) where isDir(LocalFS, c):
            FS'.Directories = FS'.Directories + (dest' + childElements(src, c))
        and forall c in descendants(LocalFS, src) where isFile(LocalFS, c):
            FS'.Files[final_name(c, dest')] = LocalFS.Files[c]
    LocalFS' = LocalFS where
        not delSrc or (delSrc = true and delete(LocalFS, src, true))

沒有預期操作隔離/原子性。這表示在操作執行期間，檔案會在來源或目的地中變更。在複製後，不保證檔案或目錄的最終狀態，只會盡力而為。例如：複製目錄時，可以將一個檔案從來源移到目的地，但沒有任何機制可以阻止複製操作仍在進行時，目的地中的新檔案被更新。

實作

預設的 HDFS 實作是遞迴尋找在 src 中找到的每個檔案和資料夾，然後將它們依序複製到最終目的地（相對於 dst）。

基於物件儲存的檔案系統應該注意上述實作產生的限制，並可以利用並行上傳和重新排序複製到儲存空間中的檔案，以最大化傳輸量。

前置條件

後置條件

result = True ==> next() will succeed.
result = False ==> next() will raise an exception

多次呼叫 hasNext()，而沒有任何介入的 next() 呼叫，必須傳回相同的值。

boolean has1 = iterator.hasNext();
boolean has2 = iterator.hasNext();
assert has1 == has2;

前置條件

hasNext() else raise java.util.NoSuchElementException

後置條件

result = the next element in the iteration

重複呼叫 next() 會傳回順序中的後續元素，直到整個順序都傳回為止。