像The Z Notation这样的形式化表示法将是定义Hadoop FileSystem行为最严格的方式，甚至可以用来证明某些公理。
然而，它存在一些实际缺陷：
这类符号的使用范围本应更广，但实际情况并非如此，因此更广泛的软件开发社区缺乏相关的实践经验。
如果不借助LaTeX 和附加库等工具，使用起来会非常困难。
这种表示方法难以理解，即使对专家来说也是如此。
鉴于本规范的目标受众是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 : 本地与运算符。在Java中表示为&&∨ : 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 data structures 被用作此语法的基础，因为它既是纯ASCII又广为人知。
[e1, e2, ... e(n)]len(L) 是指列表中元素的数量。e1 == L[0]L[0:3] == [e1,e2,e3], L[:-1] == [e1, ... e(n-1)]L' = L + [ e3 ] 进行拼接L' = L - [ e2, e1 ]。这与Python的del操作不同，后者是原地操作列表。in 当且仅当元素是列表的成员时返回真值：e2 in LL' = [ x for x in L where x < 5]L，len(L) 返回元素的数量。集合是列表符号的扩展，增加了集合中不能有重复条目且没有定义顺序的限制。
{和}大括号包围的无序项目集合。{}。这与Python不同，后者使用函数set([list])。这里的假设是集合和字典的区别可以通过内容来确定。{} 不包含任何元素。in。S' = {s for s in S where len(s)==2}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:"的部分。该部分声明的所有谓词都应该被满足，如果该部分中有指定更严格结果的条目，则应优先采用。以下是一个should前置条件的示例：
应该：
if not exists(FS, Path) : raise FileNotFoundException
在前提条件和后置条件的声明中还有进一步的条件。
supported(instance, method)该条件声明子类实现了指定的方法 - 各种FileSystem类的某些子类并未实现，而是抛出UnsupportedOperation
例如，FSDataInputStream.seek的一个前提条件是实现必须支持Seekable.seek：
supported(FDIS, Seekable.seek) else raise UnsupportedOperation