表記法

Z記法のような形式表記法は、Hadoopファイルシステムの動作を定義する最も厳密な方法であり、いくつかの公理を証明するためにも使用できます。

ただし、実際にはいくつかの欠点があります。

  1. このような表記法は、本来あるべきほど広く使用されておらず、ソフトウェア開発コミュニティ全体で実践的な経験が不足しています。

  2. LaTeX *と*アドオンライブラリのようなツールを使用せずに作業するのは非常に困難です。

  3. このような表記法は、専門家でさえ理解するのが困難です。

この仕様の対象読者がファイルシステム開発者であることを考えると、形式表記法は適切ではありません。代わりに、幅広い理解度、保守の容易さ、およびテストの容易さが、数学的に純粋な形式表記法よりも優先されます。

このドキュメントで使用されている数学記号

このドキュメントでは、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 : 論理積演算子。Javaでは、&&
  • ∨ : or : 論理和演算子。Javaでは、||
  • ∈ : in : 要素である
  • ∉ : not in : 要素ではない
  • ⊆ : subset-or-equal-to 部分集合または等しい条件
  • ⊂ : subset-of 真部分集合条件
  • | p | : len(p) 変数のサイズ

  • := : = :

  • `` : # : Pythonスタイルのコメント

  • happens-before : happens-before : Time, Clocks and the Ordering of Events in a Distributed Systemで定義されているLamportの順序関係

集合、リスト、マップ、および文字列

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コンストラクタ {} が使用されます。これは、関数 set([list]) を使用するPythonとは異なります。ここでは、集合と辞書の違いは内容から判断できるという前提です。
  • 空集合 {} には要素がありません。
  • 通常の集合の概念はすべて適用されます。
  • メンバーシップ述語は 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 <例外名> は、例外が発生することを示すために使用されます。

前提条件が満たされない場合にアクションを定義するために、if-then-elseシーケンスで使用できます。

例

if not exists(FS, Path) : raise IOException

実装が例外の集合のいずれかを発生させる可能性がある場合、これは例外の集合を提供することによって示されます。

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

例外の集合が提供される場合、集合の最初の要素は、問題の診断に役立つという理由で、後のエントリよりも優先されます。

また、満たされ*なければならない*述語と、満たされる*べき*述語を区別する必要があります。このため、関数仕様には、前提条件に「すべきこと:」とマークされたセクションが含まれる場合があります。このセクションで宣言されているすべての述語は満たされる*べき*であり、そのセクションに、より厳密な結果を指定するエントリがある場合は、それが優先される*べき*です。 should-preconditionの例を次に示します。

すべきこと

if not exists(FS, Path) : raise FileNotFoundException

条件

前提条件と事後条件の宣言には、さらに条件が使用されます。

supported(インスタンス, メソッド)

この条件は、サブクラスが指定されたメソッドを実装することを宣言します。さまざまなFileSystemクラスの一部のサブクラスは実装せず、代わりに UnsupportedOperation を発生させます。

例として、FSDataInputStream.seek の前提条件の1つは、実装が Seekable.seek をサポートしている必要があることです。

supported(FDIS, Seekable.seek) else raise UnsupportedOperation