符號

正式符號，例如 Z 符號，是定義 Hadoop FileSystem 行為的最嚴格方式，甚至可用於證明一些公理。

但是，它有一些實際上的缺陷

  1. 此類符號的使用並不如應有地廣泛，因此更廣泛的軟體開發社群不會有實際的經驗。

  2. 如果不使用 LaTeX 和附加函式庫，就非常難以使用。

  3. 此類符號難以理解，即使對專家來說也是如此。

由於此規格的目標受眾是 FileSystem 開發人員，因此正式符號並不適當。相反地，廣泛的可理解性、易於維護性和易於衍生測試優先於數學上純粹的正式符號。

本文中的數學符號

本文確實使用 Z 語法中的符號子集，但採用 ASCII 形式，並使用 Python 清單符號來操作清單和集合。

  • iff : iff 當且僅當
  • ⇒ : implies
  • → : --> 全域函數
  • ↛ : -> 部分函數

  • ∩ : ^: 集合交集

  • ∪ : +: 集合聯集
  • \ : -: 集合差集

  • ∃ : exists 存在謂詞

  • ∀ : forall: 對所有謂詞
  • = : == 等於運算子
  • ≠ : != 運算子。在 Java 中，z ≠ y 寫成 !( z.equals(y))，適用於所有非簡單資料類型
  • ≡ : equivalent-to 等價運算子。比等於更嚴格。
  • ∅ : {} 空集合。∅ ≡ {}
  • ≈ : approximately-equal-to 近似等於運算子
  • ¬ : not 非運算子。在 Java 中，!
  • ∄ : does-not-exist: 不存在謂詞。等同於 not exists
  • ∧ : and : 區域 and 運算子。在 Java 中，&&
  • ∨ : or : 區域 or 運算子。在 Java 中，||
  • ∈ : in : 元素
  • ∉ : not in : 非元素
  • ⊆ : subset-or-equal-to 子集或等於條件
  • ⊂ : subset-of 真子集條件
  • | p | : len(p) 變數大小

  • := : = :

  • `` : # : Python 式註解

  • happens-before : happens-before : Lamport 在 Time, Clocks and the Ordering of Events in a Distributed System 中定義的排序關係

集合、清單、對應和字串

本文法採用 python 資料結構 為基礎，因為它既是純 ASCII，又廣為人知。

清單
  • 清單 L 是元素的順序序列 [e1, e2, ... en]
  • 清單 len(L) 的大小是清單中元素的數量。
  • 項目可以用 0 為基礎的索引來定址 e1 == L[0]
  • Python 切片運算子可以定址清單的子集 L[0:3] == [e1,e2]，L[:-1] == en
  • 清單可以串接 L' = L + [ e3 ]
  • 清單可以移除項目 L' = L - [ e2, e1 ]。這與 Python 的 del 操作不同，後者會就地操作清單。
  • 成員關係謂詞 in 僅在元素是清單成員時傳回 true：e2 in L
  • 清單推導可以建立新的清單：L' = [ x for x in l where x < 5]
  • 對於清單 L，len(L) 會傳回元素數量。
集合

集合是清單表示法的延伸，增加了集合中不能有重複項目，且沒有定義順序的限制。

  • 集合是使用 { 和 } 大括號包圍的未排序項目集合。
  • 宣告集合時，使用 Python 建構函式 {}。這與 Python 不同，Python 使用函式 set([list])。這裡假設可以從內容判斷集合和字典的差異。
  • 空集合 {} 沒有元素。
  • 所有常見的集合概念都適用。
  • 成員關係謂詞是 in。
  • 集合推導使用 Python 清單推導。S' = {s for s in S where len(s)==2}
  • 對於集合 s，len(s) 會傳回元素數量。
  • - 算子會傳回一個新的集合，排除算子右邊集合中列出的所有項目。
對應

對應類似於 Python 字典：{“key”:value, “key2”,value2}

  • keys(Map) 表示對應中鍵的集合。
  • k in Map 成立當且僅當 k in keys(Map)
  • 空對應寫成 {:}
  • - 算子會傳回一個新的對應，排除指定鍵的項目。
  • len(Map) 會傳回對應中項目的數量。
字串

字串是使用雙引號表示的字元清單。例如："abc"

"abc" == ['a','b','c']

狀態不可變性

所有系統狀態宣告都是不可變的。

字尾「'」（單引號）用作慣例，表示操作後系統的狀態

L' = L + ['d','e']

函式規格

函式定義為一組前置條件和一組後置條件，其中後置條件定義系統的新狀態和函式的回傳值。

例外

在傳統規範語言中，前置條件定義了必須滿足的謂詞，否則會引發某些失敗條件。

對於 Hadoop，我們需要能夠指定如果未滿足規範，會導致什麼失敗條件（通常會引發什麼例外）。

符號 raise <exception-name> 用於指示要引發例外。

它可以用在 if-then-else 序列中，以定義在前置條件未滿足時執行的動作。

範例

if not exists(FS, Path) : raise IOException

如果實作可能會引發一組例外中的任何一個，則透過提供一組例外來表示。

if not exists(FS, Path) : raise {FileNotFoundException, IOException}

如果提供了例外組，則該組的較早元素優先於較晚的條目，因為它們有助於診斷問題。

我們還需要區分必須滿足的謂詞和應該滿足的謂詞。因此，函數規範可能會在標記為「應該：」的前置條件中包含一個區段，此區段中宣告的所有謂詞都應該滿足，如果該區段中有一個條目指定了更嚴格的結果，則應該優先考慮。以下是應該前置條件的範例

應該

if not exists(FS, Path) : raise FileNotFoundException

條件

在前置條件和後置條件宣告中使用了其他條件。

supported(instance, method)

此條件宣告子類別實作了命名的方法，某些 FileSystem 類別的子類別沒有實作，而是引發 UnsupportedOperation

例如，FSDataInputStream.seek 的一個前置條件是實作必須支援 Seekable.seek

supported(FDIS, Seekable.seek) else raise UnsupportedOperation