书籍详情
用TLA+定义系统：TLA+语言与工具在软硬件设计中的应用
作者：[美] 莱斯利·兰伯特（Leslie Lamport） 著，董路明，贺志平 译
出版社：机械工业出版社
出版时间：2021-04-01
ISBN：9787111678229
定价：¥139.00
购买这本书可以去
内容简介
本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。 本书分为五个部分。第一部分包含大多数程序员和工程师需要了解的有关编写系统规约（即建立模型）的所有信息；第二部分包含更高级的示例与材料，供需要进阶的读者使用；第三部分和第四部分为TLA+的参考手册，包括语言本身的定义及工具的原理与使用；第五部分介绍在基础TLA+语言上所演进出的TLA+版本2的新特性和少许变更。
作者简介
莱斯利·兰伯特（Leslie Lamport） 微软研究院的首席研究员，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
译者序
前言
致谢
部分 入门
第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
猜您喜欢
