诸如 Z 符号 等形式符号是最严格定义 Hadoop FileSystem 行为的方式,甚至可用于证明一些公理。
但是,它存在许多实际缺陷
此类符号的使用并不像它们应该的那样广泛,因此更广泛的软件开发社区不会有其实际经验。
如果不使用诸如 LaTeX 和附加库之类的工具,就很难使用它。
此类符号很难理解,即使对于专家也是如此。
鉴于本规范的目标受众是 FileSystem 开发人员,因此形式符号不合适。相反,广泛的可理解性、易于维护性和易于派生测试优先于数学上纯粹的形式符号。
本文档确实使用了 Z 语法中的符号 的子集,但使用了 ASCII 形式,并使用了 Python 列表符号来操作列表和集合。
iff
: iff
当且仅当⇒
: implies
→
: -->
全函数↛
: ->
部分函数∩
: ^
: 集合交集
∪
: +
: 集合并集\
: -
: 集合差集∃
: exists
存在谓词
∀
: forall
: 对于所有谓词=
: ==
等于运算符≠
: !=
运算符。在 Java 中,对于所有非简单数据类型,z ≠ y
写作 !( z.equals(y))
≡
: equivalent-to
等价运算符。这比 equals 更严格。∅
: {}
空集。∅ ≡ {}
≈
: approximately-equal-to
运算符¬
: not
非运算符。在 Java 中,!
∄
: does-not-exist
:不存在谓词。等同于 not exists
∧
: and
: 局部 and 运算符。在 Java 中,&&
∨
: or
: 局部 and 运算符。在 Java 中,||
∈
: in
: 元素∉
: not in
: 非元素⊆
: subset-or-equal-to
子集或相等条件⊂
: subset-of
真子集条件| p |
: len(p)
变量的大小:=
: =
:
`` : #
: Python 样式注释
happens-before
: happens-before
: Lamport 的排序关系,如 分布式系统中的时间、时钟和事件排序 中定义的
由于 python 数据结构 是纯 ASCII 且众所周知的,因此将其用作此语法的基础。
[e1, e2, ... en]
len(L)
的大小是列表中元素的数量。e1 == L[0]
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)
返回元素的数量。集合是对列表表示法的扩展,增加了集合中不允许有重复项和没有定义顺序的限制。
{
和 }
大括号中的无序项集合。{}
。这与使用函数 set([list])
的 Python 不同。此处假设可以从内容中确定集合和字典之间的差异。{}
没有元素。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 <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