符号

诸如 Z 符号 等形式符号是最严格定义 Hadoop FileSystem 行为的方式,甚至可用于证明一些公理。

但是,它存在许多实际缺陷

  1. 此类符号的使用并不像它们应该的那样广泛,因此更广泛的软件开发社区不会有其实际经验。

  2. 如果不使用诸如 LaTeX 附加库之类的工具,就很难使用它。

  3. 此类符号很难理解,即使对于专家也是如此。

鉴于本规范的目标受众是 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 且众所周知的,因此将其用作此语法的基础。

列表
  • 列表 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]
  • 对于列表 Llen(L) 返回元素的数量。
集合

集合是对列表表示法的扩展,增加了集合中不允许有重复项和没有定义顺序的限制。

  • 集合是包含在 {} 大括号中的无序项集合。
  • 声明集合时,使用 python 构造函数 {}。这与使用函数 set([list]) 的 Python 不同。此处假设可以从内容中确定集合和字典之间的差异。
  • 空集合 {} 没有元素。
  • 所有通常的集合概念都适用。
  • 成员谓词是 in
  • 集合推导使用 Python 列表推导。S' = {s for s in S where len(s)==2}
  • 对于集合 slen(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