Specifying Systems 第三章笔记

本章描述一个异步的数据传输设备，它有三个引脚val，rdy，ack。val引脚传输数据，rdy和ack引脚表示设备的传输状态。当rdy同ack相等时可以发送数据，并在发送后调整rdy为同ack不相等，等待接收方接受数据并将ack设置为相等。

规范是对系统的抽象，它试图证明在这种程度的抽象上，系统蕴含某些性质，但是它不能确保抽象没有描述的事情会怎样影响系统。优秀的工程师应当将系统的关键进行抽象，并舍弃不重要的细节。具体而言，是指选择哪些变量描述系统，以及选择什么粒度的步描述系统的变化。对本章这个设备而言，本章将发送数据和调整rdy的过程抽象为原子操作。

3.1 第一个规范

系统抽象为上述三个变量，val的取值与抽象无关，不妨假设为一个常数集合Data。这可以通过CONSTANT关键字表达

CONSTANT  Data

我们想确保变量总是满足一定的类型，这可以通过下面的公式表达。注意 TLA+ 对缩进敏感。

TypeInvariant == /\ val \in Data
                 /\ rdy \in {0, 1}
                 /\ ack \in {0, 1}

该公式又被叫做类型不变量。更正式的说，不变量是规范中定理的后件的一部分。

THEOREM specification => []invariant

一个限定变量取值集合的不变量叫做类型不变量，该集合又叫做变量的类型。

本规范的初始状态和状态转移描述较为简单，详见原书。其中使用了UNCHANGED关键字表示状态转移中某些变量不变，和<<element_1, element_2, ...>>表示元组。

3.2 另一个规范

可以把val，rdy，ack的取值封装为一个记录，val，rdy，ack是记录的域。通过record.field访问一个域。通过[field1 |-> value1, ...]表示record.field1 = value1 /\ ...。通过[field1 : type1, ...]限定域的类型。这样就可以表示为

TypeInvariant  ==  chan \in [val : Data,  rdy : {0, 1},  ack : {0, 1}]

通过action(parameter)表示带参数的动作，我们可以使用如下的动作描述发送数据时的状态转移：

Send(d) ==  /\ chan.rdy = chan.ack
            /\ chan' = [chan EXCEPT !.val = d, !.rdy = 1 - @]

其中EXCEPT与!组合表明新记录在某些域上有新取值，@表示这个域的旧值。可以验证使该动作为真的状态转移确实按照预期描述了系统。

3.3 一个关于类型的提醒

TLA+ 在编程语言的层面上是无类型的，类型不变量只是一个 TLA+ 中的公式。

3.4 定义

标识符与==右边的表达式是互为替换（前提是不破坏优先级）的关系。标识符不能重复定义。

VARIABLE和CONSTANT作用域是模块，EXTEND module可以导入其他模块的标识符到本模块。量词描述的变量、带参数标识符的形式参数，它们的作用域是该表达式。

3.5 注释

以下是两种形式的注释

(* comment *)
\* comment

注释可以嵌套。