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

出版者的话 译者序 前言 致谢 **部分 入门 第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