《中兴通讯技术丛书 计算机科学丛书 用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用》（美）莱斯利·兰伯特作；董路明，贺志平译|(epub+azw3+mobi+pdf)电子书下载

图书名称：《中兴通讯技术丛书 计算机科学丛书 用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用》

【作　者】（美）莱斯利·兰伯特作；董路明，贺志平译

【丛书名】中兴通讯技术丛书 计算机科学丛书

【页 数】 314

【出版社】 北京：机械工业出版社 , 2021.04

【ISBN号】978-7-111-67822-9

【分 类】并发程序设计

【参考文献】 （美）莱斯利·兰伯特作；董路明，贺志平译. 中兴通讯技术丛书 计算机科学丛书 用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用. 北京：机械工业出版社, 2021.04.

图书封面：

图书目录：

《中兴通讯技术丛书 计算机科学丛书 用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用》内容提要：

本书系统介绍了形式化建模语言TLA+以及模型检查工具TLC，并结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。本书分为五个部分。第一部分包含大多数程序员和工程师需要了解的有关编写系统规约（即建立模型）的所有信息；第二部分包含更高级的示例与材料，供需要进阶的读者使用；第三部分和第四部分为TLA+的参考手册，包括语言本身的数学定义及工具的原理与使用；第五部分介绍在基础TLA+上所演进出的TLA+版本2的新特性和少许变更。本书适合高级软硬件开发设计人员、测试人员、架构师以及相关学术研究人员阅读。

《中兴通讯技术丛书 计算机科学丛书 用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用》内容试读

第一部分

Specifying Systems:The TLA*Language and Tools for Hardware and Software Engineers

人

门

系统规约是由大量普通数学公式和极少量时态逻辑公式组成的，这也是大部分TLA+

结构被用来表示普通数学的原因，你必须熟悉普通数学才能写好规约。不幸的是，很多大

学的计算机学院似乎认为让学生熟练掌握C++比拥有坚实的数学基础更重要。因此，很

多读者可能不太熟悉编写系统规约所需要的数学基础。不过幸运的是，这些数学知识都比

较简单。只要学习C++没有摧毁你的逻辑思维能力，学习这些知识就不会有任何障碍。假

定你在接触C++之前已经学会了算术，掌握了数和基于数的四则运算日，接下来我会试

着讲解其他所需的数学概念，第1章是对所需基础数学知识的复习，我希望大部分读者在读下来后会发现这一章完全不必要。

在第1章对普通数学的简单回顾之后，第2心5章是一系列运用TLA+的简单例子，

第6章是编写规约所需的更深一点的数学知识，第7章是对之前知识的回顾，并提供了一些编写规约的建议。学完这一章之后，你应该已经掌握了在一般工程实践中编写规约可能遇到的大部分问题的解决办法。

日部分读者可能需要回顾一下，数不是bit串，233×233等于266，且不会溢出。

第1章

Specifying Systems:The TLA*Language and Tools for Hardware and Software Engineers

简单数学基础

1.1命题逻辑

初等代数是研究实数及+、一、*（乘）和/（除）四则运算的数学。命题逻辑是研究

两个布尔值TRUE和FALSE及其5种运算的数学分支，这5种运算分别是：

∧合取(and)

→蕴涵(implies)

V析取(or)

≡等价(is equivalent to)

否定(not)

为了学习如何算数，你必须记住加法和乘法表以及多位数运算法则。命题逻辑要简单

得多，因为其只有两个值：TRUE和FALSE。要学习如何计算布尔值，你只需要知道以下5

个布尔运算符的定义：

∧：FAG为TRUE当且仅当F和G都为TRUE。

V:FVG为TRUE当且仅当F或G为TRUE(或均为TRUE)。

:F为TRUE当且仅当F为FALSE。

→：F→G为TRUE当且仅当F为FALSE或G为TRUE(或均为TRUE)。

≡：F三G为TRUE当且仅当F和G都为TRUE或都为FALSE。

和大多数数学家一样，我使用或时意味着和/或。

我们也可以用真值表来表示这些运算符。下面这个真值表给出了F→G对于F和

G的所有四种真值组合的值：

F

G

F→G

TRUE

TRUE

TRUE

TRUE

FALSE

FALSE

FALSE

TRUE

TRUE

FALSEFALSE

TRUE

公式F→G断言了F蕴涵G,也就是说，F→G为真当且仅当语句“F蕴涵G”为

真。人们常常对→运算符感到困惑，不明白为什么FALSE→TRUE和FALSE→FALSE都

为TUE。要解释这一点其实很简单，在我们的认知中，因为如果n大于3，那么它必然大于1，所以n>3就意味着（蕴涵）n>1,因此，公式(n>3)→(n>1)为TUE。在这

第1章简单数学基础3

个公式中将4、2、0分别代入，就可以解释为什么F→G意味着F蕴涵G,或者等价

地，如果F为真，那么G为真。

等价运算符三只用于布尔等式中。我们可以用=代替三，但不能反过来（例如，我

们可以写FALSE=一TRUE,但不能写2+2三4)。在布尔表达式中用三=代替=，表述会

比较清晰9。

就像代数公式一样，命题逻辑公式是由数值、运算符和变量（如x)组成的。不过，命

题逻辑公式只能使用TRUE和FALSE这两个值，以及5个布尔运算符(A、V、一、→和三)。

在代数公式中，*与+相比具有更高的优先级（结合更紧密），因此x十y*之表示x+(y*之)。

类似地，在命题逻辑公式中，一的优先级比∧和V高，而∧和V的优先级又比→和三高，

因此一F∧G→H表示(（一F)∧G)→H。其他数学运算符（如+和>）的优先级高于命题

逻辑运算符，因此n>0→n-1≥0表示(n>0)→(n-1≥0)。多余的括号不会影响阅读，反而会更有助于阅读和理解公式，如果你对是否需要括号有一点怀疑，就使用它们。运算符∧和V是满足结合率的，就像+和*一样。+满足结合率意味着x+(y+2)等于(x+)+z,因此我们可以不用括号来表示x+y+之。类似地，A和V的结合律让

我们可以直接写FAGAH或FVGVH。类似+和*，运算符A和V也是满足交换律

的，因此F∧G等价于G∧F,FVG等价于GVF。

为了判定公式(x=2)→(x+1=3)是否为真，我们必须了解算术的一些基本性质。然而，我们可以说(x=2)→(x=2)V(y>7)为真，即使我们对x和y的取值一无所知。

这个公式为真，是因为F→FVG为真，不论F和G是什么公式。换句话说，F→FVG

对于F和G的所有可能取值都为真。这种公式称为重言式(tautology)。

般来说，命题逻辑重言式是一个对于其变量的任何可能取值都为真的命题逻辑公式。

像这样简单的重言式和基于数的简单代数性质一样明显。F→FVG为重言式与“对于所

有非负数x和y,x≤x+y为真”是一样显而易见的。我们可以通过计算从简单的重言式推导出复杂的重言式，正像可以从简单的四则运算推导出复杂的数学性质一样。但是，这些都需要练习。你可能花了数年的时间学习如何计算数值表达式，例如，推导x≤一x+y与2*x≤y等价，但你可能还没开始学习如何推导一FVG与F→G等价。

如果你还没学会如何计算布尔表达式，可能就得靠类似数手指的方式来计算了，例如，通过遍历布尔变量的所有可能取值对公式进行求值，来检查该公式是否是重言式。上述操作最好通过构造一个真值表来完成，该真值表列出变量可能的取值并给出所有子公式的对

应值。例如，下面的真值表表示(F→G)≡（一FVG)是重言式：

F

G

F→G

F

FVG(F→G)≡一FVG

TRUE

TRUE

TRUE

FALSE

TRUE

TRUE

TRUE

FALSE

FALSE

FALSE

FALSE

TRUE

FALSE

TRUE

TRUE

TRUE

TRUE

TRUE

FALSEFALSE

TRUE

TRUE

TRUE

TRUE

日16.1.3节解释了使用三代替=表示布尔值相等的更微妙的原因。

4第一部分入门

编写真值表是加强对命题逻辑理解的好方法。但是，在进行这种计算时，计算机要比

人类做得更好。在15.6.3节的最后将说明如何使用TLC模型检查器来验证命题逻辑重言

式和执行其他TLA+计算。

1.2集合

集合论是普通数学的基础。集合通常被描述为元素的“聚合”(collection),但是说集合是聚合也不是特别准确，集合的概念如此基础以至于我们不会试图去定义它。我们先把集合和关系∈作为未定义的概念，其中x∈S表示x是S的一个元素，我们常说“在集合S中”(isin),而不是“是S的一个元素”(is an element of).

一个集合可以有有限数量的元素，也可以有无限数量的元素。所有自然数(0、1、2等)的集合是一个无限的集合。比3小的自然数组成的集合是有限集，包含了0、1和2这三个元素，我们可以将之记作集合{0,1,2}。

一个集合完全取决于它的元素。两个集合相等当且仅当它们拥有相同的元素。因此，{0,1,2}、{2,1,0}和{0,0,1,2,2}是相同的集合，即拥有三个元素0、1、2的集合。空集记作{}，是唯一一个拥有0个元素的集合。

常用的集合操作如下：

∩交集U并集

二子集\差集

下面是定义和运用示例：

S∩T:S和T中都包含的元素的集合。

{1,-1/2,3}∩{1,2,35,7}={1,3

SUT:S或T中包含（也可以都包含）的元素的集合。

{1,-1/2}U{1,5,7}={1,-1/2,5,7

SCT:值为真当且仅当S中的元素也都是T中的元素。

{1,3}c{3,2,1

S\T:在S中但不在T中的元素的集合。

{1,-1/2,3}1{1,5,7}={-1/2,3}

这就是在开始学习如何定义系统之前，我们需要了解的关于集合的所有信息了，我们将在6.1节中继续讨论集合论。

1.3谓词逻辑

一旦有了集合，我们就可以很自然地说某个公式对于集合的所有元素或者部分元素为真。谓词逻辑在命题逻辑的基础上引入了两个量词(quantifier):

V:全称量词(for all),用于全称量化。3:存在量词(there exists.),用于存在量化。·

···试读结束···