本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。
用形式化的建模和验证方法保证所设计的软硬件系统的正确性
本书将指导你如何使用TLA+语言编写计算机系统规约。全书篇幅比较长，但大多数人只需要阅读第一部分的内容就够了，这部分包含了大多数工程师需要了解的与编写规约有关的知识，至于学习它所需要的背景知识，只要求具备工程学或计算机科学的本科生所应掌握的数学和计算机知识即可。第二部分将为需要进阶的读者提供更深入的内容。本书的其余部分是参考手册——第三部分介绍TLA+工具，第四部分介绍TLA+语言本身。
TLA官网http://lamport.org有可供下载的配套资源，包括TLA+工具、练习、参考资料和勘误清单。你也可以在搜索引擎上输入uidlamporttlahomepage来找到上述页面，但请不要把这个字符串放到互联网上共享。
何为规约
写作是发现你的想法有多么草率的根本方法。
——Guindon
规约是“系统应该做什么”的书面定义。定义一个系统有助于我们更好地理解它。在构建系统之前最好先理解该系统，因此在实现之前先编写系统规约是个好主意。
本书讲述了系统的行为属性，也可称之为功能属性或逻辑属性。这些属性定义系统应该做什么。当然系统还有其他我们这里不考虑的重要属性，比如性能属性。最差情况下的性能通常可以表示为行为属性，在第9章我们讲述了如何定义系统在一定时间内的行为，不过，本书暂时不考虑如何定义平均性能。
我们编写规约的基本工具是数学。数学是一门严谨的语言，比自然语言（例如英语或中文）更为精准。在工程实践中，不精准就很容易出错，因此科学和工程学通常采用数学作为基本语言。
本书用到的数学语言会比你一直使用的数学语言更形式化一些。相对于形式化数学，大多数数学家和科学家在写作中使用的数学表达方式并不十分精准，应用于小范围还勉强可以，应用于大范围则不佳。在非形式化数学语言中，每个方程都是一个精确的断言，但你必须阅读方程前后的解释性文字才能理解方程之间的关系以及定理的确切含义。逻辑学家已经研究出了消除这些解释性文字并使数学更形式化、更精准完备的方法。
大多数数学家和科学家可能认为形式化数学又长又乏味，这是不对的，普通数学也可以用一种精准完备的形式化语言来简洁表达。例如在第11章关于微分方程的Diffeential-Equations模块中，只需要用20多行就可以定义任意微分方程的解。不过很少有规约需要用到如此深奥的数学知识，大多数时候只需要简单应用一些基础数学概念即可。
为何是TLA+
我们通过描述在执行过程中可能会发生的行为来定义系统。1977年，AmirPnueli引入了时态逻辑（temporallogic）来描述系统行为。从理论上讲，系统可以用单个时态逻辑公式表示，但在实际运用上却有些问题：它虽然能很理想地描述系统的某些属性，但在描述其他属性上却不太方便。因此，我们通常将它与更传统的系统表示方式结合在一起来定义系统。
也可称为时序逻辑或时间逻辑，在本书中为了术语统一，均译为时态逻辑。——译者注
在20世纪80年代后期，我发明了TLA，即基于动作（Action）的时态逻辑——这是Pnueli初始逻辑的简单变体。TLA使得用单个公式表示系统变得切实可行。TLA规约的大部分由普通的、非时态逻辑的数学公式组成，时态逻辑仅在其擅长描述的属性中引入并发挥作用。TLA还给出了一种很友好的系统推理模式，这种模式被称为断言式推理（assertionalreasoning），其在实践中被证明是最有效的。不过，本书仅涉及规约本身，较少引入数学证明。
TLA+版本2对证明做了大量改进，参见19.7节。——译者注
时态逻辑使用了一套基本逻辑来表示普通数学，还有许多其他方法也可以使普通数学形式化。大多数计算机科学家都喜欢使用与他们熟悉的编程语言近似的语言，相反，我选择了大多数数学家更喜欢的方法，逻辑学家将其称为一阶逻辑和集合论。
TLA为描述系统提供了数学基础。要编写规约，我们需要在此基础上构建完整的语言体系。我最初认为该语言应该是某种抽象的编程语言，其语义将基于TLA。一开始我不知道用哪种编程语言结构最好，于是决定直接用TLA编写规约，计划在需要时再引入编程语言。令我惊讶的是，到后来我发现不需要了，我所需的就是一种编写数学公式的健壮语言。
尽管数学家已经发展了编写公式的科学，但他们还没有将其转化为工程学科，他们为小规模的数学模型开发了符号语言，但对于大型应用还没有好的方法，因为真实系统的规约可能长达数十页甚至数百页。数学家知道如何编写20行的公式，但对长达20页的公式却束手无策。因此，我不得不在语言中引入书写长公式的符号方法，这些方法的形成得益于我从编程语言中学到的将大型规约模块化的思路。
我将这种语言称为TLA+。在编写不同离散系统的规约时，我不断对TLA+进行提炼和改进，直到后来TLA+趋于稳定。我发现TLA+可以很好地定义从应用程序接口（API）到分布式系统的各种系统。它可以用来为几乎任何类型的离散系统编写精准的形式化定义，尤其适合描述异步系统，即组件运行不严格遵循锁步操作（lock-step）的系统。
关于本书
本书的第一部分包括第1～7章，是本书的核心，需要从头到尾阅读。它描述了如何定义称为安全属性的一类属性，这也是大多数工程师在编写规约时需要熟知的，定义这些属性几乎不需要用到时态逻辑。
阅读完第一部分后，你可以根据自己的需要阅读第二部分，它的每一章都是独立的：第8章详细介绍时态逻辑，时态逻辑被用来定义活性属性；第9章介绍如何定义实时属性；第10章介绍如何编写组合规约；第11章包含更多高级示例。
第三部分包含了三种TLA+工具的参考手册：语法分析器、TLATEX排版程序和TLC模型检查器。使用TLA+需要用到这些工具，你可从TLA官网下载它们。三个工具中TLC是最复杂的，Web上的示例可以帮助你入门，但要深入学习如何有效运用TLC，必须阅读第14章。
第四部分是TLA+语言的参考手册。第一部分已经为TLA+的大多数用途提供了足够实用的语言知识，因此仅在对语法和语义的关键点有疑问时才需要阅读第四部分。第15章介绍TLA+的语法。第16章介绍TLA+所有内置运算符的确切定义和一般形式。第17章介绍所有更高级别的TLA+语言构成（例如定义）的确切含义。第16章和第17章共同描述TLA+的语义。第18章介绍标准模块（不包括第9章介绍的RealTime模块和第14章介绍的TLC模块），如果你对如何用TLA+语言将标准的基础数学形式化有兴趣，不妨参阅本章。
第四部分有一些你可能需要经常翻阅的内容：一份迷你手册，简要介绍了许多有用的信息。该部分的开篇列出了所有TLA+运算符、用户可自定义的符号、运算符的优先级、标准模块定义的所有运算符，以及诸如?等符号的ascii表示。
第五部分介绍TLA+版本2。其中新加入的大部分特性都与定理及证明有关，这些定理可以由TLA+定理系统TLAPS验证。与规约有关的最大变化是递归运算符定义和lambda表达式的引入。另外，第19章还有一节重点说明了如何为子表达式命名。
计算机\分布式
TLA+代表了我所见过的唯一一种可视化和量化算法复杂度的有效方法，这种方法对工程师来说很有意义。
—— Brannon Batson，英特尔公司处理器架构师
本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。
本书分为五个部分。第一部分包含大多数程序员和工程师需要了解的有关编写系统规约（即建立模型）的所有信息；第二部分包含更高级的示例与材料，供需要进阶的读者使用；第三部分和第四部分为TLA+的参考手册，包括语言本身的定义及工具的原理与使用；第五部分介绍在基础TLA+语言上所演进出的TLA+版本2的新特性和少许变更。
作者简介
莱斯利·兰伯特（Leslie Lamport） 微软研究院的首席研究员，2013年图灵奖得主，美国国家科学院和国家工程院院士，LaTeX系统创始人。他是拥有杰出贡献和辉煌成就的计算机大师、分布式系统领域的先锋人物，他的分布式计算理论奠定了计算机学科的基础。他于1978年发表的论文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持着计算机科学史上的被引用量纪录。
最初接触到TLA+，缘起于网络安全相关的工作。业界对于如何保证信息系统行为的完备性和正确性以及如何避免设计阶段的逻辑缺陷所导致的安全漏洞，一般都采用所谓的形式化验证技术。形式化验证技术一直应用于操作系统内核、交通控制系统、航空航天系统、大型分布式数据库、区块链等具有高安全性、高可靠性要求的关键信息系统的开发设计中。但随着时代的发展，人们对小到智能终端、大到政府机构服务网站等各种信息系统的依赖越来越强，而这些系统也不再像传统信息系统那样封闭，它们面临的挑战和威胁与日俱增。为此，对于所谓的“非关键”信息系统而言，通过形式化技术提高设计质量、保证安全性与可靠性的需求也变得越来越迫切。
TLA+就是一种非常优秀的形式化建模语言。它的优点首先在于通用性，它可以描述大多数离散事件系统的行为逻辑，并且不与具体的行业应用紧耦合。其次，它的难度适中，仅涉及CS专业大学本科阶段的数学和计算机科学知识，能够被广大开发与设计人员所掌握。而且由于作者的精心设计，它在验证高并发、分布式等复杂逻辑方面具有独特的优势。
译者所就职的中兴通讯是一家通信设备研发制造企业，针对5G无线通信系统的开发与设计，要满足99.999％的可靠性指标，即系统在连续1年的运行过程中，最多允许有5分钟时间不能正常提供服务，其他时间必须保证安全、可靠地持续提供服务。为此，我们所在的团队使用TLA+对其中的部分关键模块实施了验证，并取得了良好的效果。在学习和实践TLA+的过程中，我们也遇到了一些困难和障碍，其中之一就是中文资料匮乏，只能参考作者官网主页上的英文资料和帮助文档，以及向公司内一些有经验的同事请教。由于TLA+本质上是一种数学建模语言，它本身存在一定的学习门槛，所以分析人员必须要具备对TLA+原理的深入理解才能有效开展对工程复杂问题的分析和验证。而花时间仔细研读原版资料固然可以掌握其精髓，但却无法解决知识域的快速传播与扩散的问题。为了使业界更多的开发和设计人员能够快速掌握TLA+这个利器，并解决“知其然不知其所以然”的困惑，我们便萌生了翻译本书的想法，希望能为该技术在国内的推广使用尽一份绵薄之力。
本书是作者25年研究成果的总结，它包含了TLA+语言和验证工具原理与实践的介绍，并结合具体的实践案例提供了循序渐进的使用指导，既适合初级读者入门，也适合进阶读者研究参考。在中文版中，译者应作者本人的要求，添加了当前英文版中未包含的关于TLA+版本2新特性的描述，并修订了英文版自出版以来的所有勘误内容。
翻译过程是漫长而艰苦的，自开始翻译到定稿，中间断断续续持续了约半年时间，曾有好几次因工作冲突而暂停，但我们最终还是坚持了下来。这项工作的最终完成，离不开公司相关领导和同事的大力支持，在这里首先要感谢中兴通讯学院的闫林院长，是他为我们联系了机械工业出版社，同时也要感谢无线产品经营部的龚明部长、王碧波部长、刘志华科长与范璟玮总监，是他们为我们的翻译工作提供了各种便利与帮助。最后，还要感谢作者，是他在得知我们的翻译意向后，热心协调，为我们解决了版权授权的问题，并为我们提供了原始手稿的tex源文件，极大地提高了我们的翻译效率。
本书的翻译由贺志平、董路明完成，其中贺志平翻译了第1～9章、第14章以及第10章与第19章的部分内容，董路明翻译了第11～18章（第14章除外）以及第10章与第19章的剩余内容。由于我们也是TLA+技术的新手，翻译过程中难免会有一些错误和问题，还希望各位读者批评和指正。如果你觉得翻译中有任何错误和问题，请务必反馈给我们，以便及时进行修正。
最后，针对TLA+相关的问题和疑惑，读者也可以在作者的个人主页（http://lamport.azurewebsites.net/tla/tla.html）与Google社区上的TLA+论坛（https://groups.google.com/g/tlaplus）上寻求帮助。这里要特别强调一下Google社区上的TLA+论坛，该论坛活跃度很高，有大量高水平的成员参与，且对于具体技术问题的回帖响应非常及时，有志于研究TLA+技术的读者一定要善于使用该资源。
董路明 贺志平
2020 年 10 月 20 日
出版者的话
译者序
前言
致谢
第一部分 入门
第1章 简单数学基础2
1.1 命题逻辑 2
1.2 集合4
1.3 谓词逻辑 4
1.4 公式与陈述句 6
第2章 定义一个简单时钟 7
2.1 行为7
2.2 时钟7
2.3 解读规约 9
2.4 TLA+ 规约 10
2.5 规约的另一种写法 12
第 3 章 异步接口示例 13
3.1 第一个规约14
3.2 另一个规约17
3.3 类型回顾 18
3.4 定义 19
3.5 注释 20
第 4 章 FIFO 接口示例23
4.1 内部规约 23
4.2 剖析实例化25
4.2.1 实例化是一种代换 25
4.2.2 参数化的实例化 26
4.2.3 隐式代换 26
4.2.4 不需重命名的实例化 27
4.3 隐藏内部变量 27
4.4 有界 FIFO 28
4.5 我们在定义什么 30
第 5 章 缓存示例31
5.1 内存接口 31
5.2 函数 33
5.3 可线性化内存系统 35
5.4 元组也是函数 37
5.5 递归函数定义 38
5.6 直写式缓存39
5.7 不变式 44
5.8 证明实现 45
第 6 章 数学基础拓展 47
6.1 集合 47
6.2 “笨表达式” 48
6.3 递归回顾 49
6.4 函数与运算符 51
6.5 函数使用 53
6.6 choose 54
第 7 章 编写规约：一些建议 55
7.1 为什么要编写规约 55
7.2 我们要定义什么 55
7.3 原子粒度 56
7.4 数据结构 57
7.5 编写规约的步骤 57
7.6 进一步提示58
7.7 定义系统的时机和方法 60
第二部分 更多高级主题
第 8 章 活性和公平性 64
8.1 时态公式 64
8.2 时态重言式68
8.3 时态证明规则 71
8.4 弱公平性 71
8.5 内存规约 75
8.5.1 活性要求 75
8.5.2 换个表示法 76
8.5.3 推广80
8.6 强公平性 81
8.7 直写式缓存82
8.8 时态公式量化 84
8.9 时态逻辑剖析 85
8.9.1 回顾85
8.9.2 闭包85
8.9.3 闭包和可能性 87
8.9.4 转化映射和公平性 87
8.9.5 活性不重要 89
8.9.6 时态逻辑让人困惑 89
第 9 章 实时系统90
9.1 回顾时钟规约 90
9.2 通用实时规约 93
9.3 实时缓存 96
9.4 Zeno 规约100
9.5 混合系统规约 102
9.6 关于实时103
第 10 章 组合规约 104
10.1 双规约的组合 104
10.2 多规约的组合 107
10.3 FIFO 109
10.4 共享状态的组合 111
10.4.1 显式状态变化 112
10.4.2 相交动作的组合 114
10.5 简短回顾118
10.5.1 组合方法的分类 118
10.5.2 审视交错规约 118
10.5.3 审视相交动作规约 118
10.6 活性和隐藏 119
10.6.1 活性和闭包119
10.6.2 隐藏 120
10.7 开放系统规约 121
10.8 接口转化123
10.8.1 二进制时钟123
10.8.2 转化通道125
10.8.3 接口转化推广 128
10.8.4 开放系统规约 129
10.9 规约形式选择 131
第 11 章 高级示例 132
11.1 定义数据结构 132
11.1.1 局部定义132
11.1.2 图 134
11.1.3 求解微分方程 137
11.1.4 BNF 语法139
11.2 其他内存系统的规约 145
11.2.1 接口 146
11.2.2 正确性条件147
11.2.3 串行内存系统 148
11.2.4 顺序一致内存系统 155
11.2.5 对内存规约的思考 161
第三部分 工具
第 12 章 语法分析器 164
第 13 章 TLATEX 排版器 166
13.1 引言 166
13.2 阴影效果的注释 167
13.3 规约排版168
13.4 注释排版168
13.5 调整输出格式 170
13.6 输出文件170
13.7 故障定位172
13.8 使用 LATEX 命令 172
第 14 章 TLC 模型检查器 174
14.1 TLC 介绍174
14.2 TLC 的应用范围 181
14.2.1 TLC 值181
14.2.2 TLC 如何计算表达式 182
14.2.3 赋值与代换184
14.2.4 计算时态公式 186
14.2.5 模块覆盖187
14.2.6 TLC 如何计算状态 187
14.3 TLC 如何检查属性190
14.3.1 模型检查模式 190
14.3.2 仿真模式192
14.3.3 视图和指纹192
14.3.4 利用对称性193
14.3.5 活性检查的限制 195
14.4 TLC 模块 196
14.5 TLC 的用法 198
14.5.1 运行 TLC 198
14.5.2 调试规约200
14.5.3 如何高效使用 TLC 204
14.6 TLC 不能做什么 207
14.7 附加说明208
14.7.1 配置文件语法 208
14.7.2 TLC 值的可比性 209
第四部分 TLA+ 语言
第 15 章 TLA+ 语法 218
15.1 简化语法218
15.2 完整的语法 226
15.2.1 优先级与关联性 226
15.2.2 对齐 229
15.2.3 注释 230
15.2.4 时态公式231
15.2.5 两种异常231
15.3 TLA+ 的词素 232
第 16 章 TLA+ 的运算符 233
16.1 恒定运算符 233
16.1.1 布尔运算符234
16.1.2 选择运算符236
16.1.3 布尔运算符的解释 237
16.1.4 条件构造239
16.1.5 let/in 构造 240
16.1.6 集合运算符240
16.1.7 函数 242
16.1.8 记录 245
16.1.9 元组 246
16.1.10 字符串 247
16.1.11 数字 248
16.2 非恒定运算符 249
16.2.1 基础恒定表达式 249
16.2.2 状态函数的含义 250
16.2.3 动作运算符251
16.2.4 时态运算符254
第 17 章 模块的含义 257
17.1 运算符与表达式 257
17.1.1 运算符的元数与顺序 257
17.1.2 λ 表达式 258
17.1.3 简化运算符应用 259
17.1.4 表达式 260
17.2 级别 261
17.3 上下文 263
17.4 λ 表达式的含义 264
17.5 模块的含义 265
17.5.1 引入 266
17.5.2 声明 266
17.5.3 运算符定义267
17.5.4 函数定义267
17.5.5 实例化 267
17.5.6 定理与假设269
17.5.7 子模块 269
17.6 模块的正确性 270
17.7 寻找相关模块 270
17.8 实例化的语义 271
第 18 章 标准模块 276
18.1 Sequences 模块276
18.2 FiniteSets 模块 277
18.3 Bags 模块277
18.4 关于数字的模块 279
第五部分 TLA+ 版本 2 基础
第 19 章 TLA+ 版本 2 286
19.1 简介 286
19.2 递归运算符定义 286
19.3 lambda 表达式 288
19.4 定理与假设 288
19.4.1 命名 288
19.4.2 assume/prove 289
19.5 实例化 290
19.5.1 实例化词缀运算符 290
19.5.2 Leibniz 运算符和实例化 291
19.6 命名子表达式 292
19.6.1 标签和带标签的子表达式 名称 292
19.6.2 位置相关的子表达式名称 294
19.6.3 let 定义中的子表达式 297
19.6.4 assume/prove 的子表达式 297
19.6.5 将子表达式名称用作运算符 298
19.7 证明的语法 298
19.7.1 证明的结构298
19.7.2 use、hide 与 by 300
19.7.3 当前状态302
19.7.4 具有证明的步骤 303
19.7.5 无证明的步骤 306
19.7.6 对步骤与其组成部分的引用 308
19.7.7 对实例化的定理的引用 310
19.7.8 时态证明311
19.8 证明的语义 311
19.8.1 布尔运算符的含义 311
19.8.2 assume/prove 的含义 312
19.8.3 时态证明312
