对于一套系统的设计，通常我都是想好了，然后直接捋起袖子写代码了。 写完了，在开始加很多 test 来保证它的正确性。 但其实，我并不能保证设计是完全正确的。也就是说，我的实现满足了该系统的需求，但也有可能在一些 corner case 上面并没有考虑周全。 同时， 虽然后面可以写很多 test，但并
本节定义了一个内存系统的通用接口，给出了其设计考虑，并重点说明了为什么以及如何将一个表达式声明为常量参数。 声明：CONSTANT Send(_,_,_,_)\text{CONSTANT } Send(\_, \_, \_, \_)CONSTANT Send(_,_,_,_) 类型假设：ASSUME ∀p,d,miOld,miNew:Send(p,d,miOld,miNew)∈BOO
本节详细说明了模块实例化的几个方面： 实例化本质上是一种代换，通过代换待实例化模块中的符号，最终得到的表达式只包含TLA+TLA^+TLA+的内建运算符和当前模块定义的常量和参数； 也可以将实例作为入参，这样只需要一条实例化定义语句即可； 一条INSTANCE\text{INSTANCE}INSTANCE语句
下一个例子是FIFO缓冲区，简称FIFO，它是一个装置，发送方进程使用它向接收方传输一系列的值。发送方和接收方使用ininin和outoutout两个通道与缓冲区通信: 值的发送将遵循第30页图3.2中的ChannelChannelChannel模块指定的异步协议。该系统规约将允许下列行为：其步骤中具有四种非
