7.1 为什么写规范

  • 在实现前、在设计阶段发现错误

  • 精确、清晰地描述系统

  • 应用工具自动化检查

7.2 去规范什么

写规范的主要目的是暴露错误，TLA+ 擅长处理并发场景，因此应当主要用作暴露并发错误。

7.3 原子性的粒度

使用什么粒度描述系统通常需要经验的积累，这里有一个经验：

在某种粒度上，系统的状态转移如果是可交换的，并总能将步1与步2交换到相邻位置，那么就可以把步1和步2组合为一个步。

7.4 数据结构

再次强调，写规范的主要目的是暴露错误，如果内存布局、数据结构等信息并不会出错，就无须在规范中指明。例如第五章使用Send运算符描述系统的状态转移，没有深入到系统如何实现Send之中。

7.5 写一个规范

在此总结一下写规范的步骤：

  1. 选择要描述的系统组件和抽象层级

  2. 选择变量表示系统状态，定义不变量、初始状态，此时可能需要定义额外的常量和假设

  3. 描述状态转移，尽量做到紧凑、容易阅读

  4. 描述时序逻辑特性，这会在第八章介绍

  5. 描述系统的性质作为定理

7.6 更多提示

不要自作聪明

指定变量的新值时，要注意最好使用v1' = exp或v2' \in exp的合取形式，而且exp中不能出现不确定的'变量。

类型不变量不是假设

要留意类型不变量中对变量类型做出的限制，其他公式是不知道的。例如

action1 == (n' > 7) /\ ...
action2 == (n' <= 6) /\ ...
Next == (n \in Nat) /\ (action1 \/ action2)

不要遗漏这里的n \in Nat。

不要过于抽象

以一个获取键盘输入的规范为例，要考虑到同时按下多个键的情况。规范过于抽象会忽视真实系统的一些状态。

有的值不能比较

TLA+ 不能判断两个不同类型值不相等。

把量词提到外层

量词提到子公式的外层能提升可读性。

注意'的对象

op(a) == x + a

对于上面运算符

op(y)' = (x + y)' = x' + y'
op(y') = x + y'

而op'(y)有语法错误，'只能应用在表达式上。

注释就写成注释

注释不要通过/\ FALSE等表达写成规范的一部分。

7.7 何时写规范，如何写规范

最好在实现系统之前明确规范。规范可以先仅描述部分特性，即使这样也可以利用工具检查一些错误。