用TLA+定义系统：TLA+语言与工具在软硬件设计中的应用

图书标准信息

• 作者 [美]莱斯利·兰伯特（Leslie Lamport）
• 出版社 机械工业出版社
• 出版时间 2021-04
• 版次 1
• ISBN 9787111678229
• 定价 139.00元
• 装帧 其他
• 开本 16开
• 纸张 胶版纸
• 页数 328页
• 字数 170千字

【内容简介】

本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。

【作者简介】

:
    莱斯利·兰伯特（Lesie Lampot）微软研究院的首席研究员，2013年图灵奖得主，美国国家科学院和国家工程院院士，LaTeX系统刨始人。他是拥有杰出贡献和辉煌成就的计算机大师、分布式系统领域的先锋人物，他的分布式计算理论奠定了计算机学科的基础。他于1978年发表的论文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持着计算机科学史上的被引用量纪录。

【目录】

出版者的话 

译者序 

前言 

致谢 

第一部分 入门 

第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