• 3 State Machines
  • 3.1 The Standard Model
  • 3.2 State Machines
  • 3.3 A Tiny Example
    • 3.3.1 Program
    • 3.3.2 Label
    • 3.3.3 Describing a State Machine with Natural Language
    • 3.3.4 Describing a State Machine with Math
    • 3.3.5 Model Check
  • 3.4 Die Hard Problem
    • 3.4.1 Problem
    • 3.4.2 Behavior
    • 3.4.3 Specification
    • 3.4.4 Model Check
    • 3.4.5 Summary
  • 3.5 Property
  • 3.6 Invariant and Inductive Invariant
    • 3.6.1 Concepts
    • 3.6.2 Euclid's Algorithm
    • 3.6.3 Invariant
    • 3.6.4 Inductive Invariant
    • 3.6.5 Lamport Papers
  • 3.7 Reference

3 State Machines

下面进入到动态部分，把State Machines的部分形式化出来。就像我们表达静态逻辑一样，我们希望用一个逻辑公式把整个系统的行为描述出来。

3.1 The Standard Model

先定义一下什么是标准模型，是TLA+中的定义。

一个抽象系统可以是一个计算机、一个钟表、一个算法、一个集群等一切能够进行计算的系统，在TLA+里通称为"抽象系统"。这个系统可以描述为一组行为，行为的Collection。为什么没用Set？因为Collection比Set要大。每一个行为表示了系统的一种可能执行。什么是行为？行为是一个状态的序列。每个状态包含了一些变量，这里的变量不是编程语言的变量，而是物理学家描述一个天体运动时的变量的概念。变量可以在不同的状态下有不同的值。在这个状态里给这些变量赋了什么值决定了这个状态。一个系统就是一组行为，每个行为表示了这个系统的可能执行，即一个状态迁移序列。一个行为是由一串状态组成。我们后面所有的工作就是：如何定义变量。不同的系统变量不一样。如何描述一个系统？为了建立这个系统的行为模型，需要哪些变量？例如，如果想描述地球围着太阳转，不需要描述所有变量，地球哪里长了一棵树肯定是不用管的。可以把地球看作一个点，只管坐标就行了。但如果想建模地球里更细的东西的话，例如河流如何运动，那就要考虑河流的弯曲程度、当前水流速度等。但如果我要考虑地球围着太阳转，肯定不考虑这些。这就是抽象层次，抽象层次决定了我们去选择哪些变量。另外，Step的大小也是我们要考虑的因素。在用TLA+建模一个系统的模型的时候，一个是选择哪些变量，一个是Step大小。这是两个重点。

这是标准模型，其实就是一个状态机的描述。

3.2 State Machines

什么是状态机？

• 它有所有可能的初始状态。
• 那些满足Next公式的状态迁移。
• 一个状态是给变量的一次赋值。

这是比前面更细致的描述，描述了其中一个行为。

如何描述一个状态机？

• 变量是什么。
• 变量可能的初始值，其实是过滤条件。
• 变量在当前状态下的值和next状态的可能值之间的关系。

3.3 A Tiny Example

3.3.1 Program

这个例子来自于Lamport的教学Videos。这是C语言程序。someNumber()是一个函数，不用管它是什么，它返回一个值，假设这个值的范围是0到1000，返回哪一个值不知道。

如何用标准模型来描述这个程序的行为呢？我们在思考如何转成一个很高层的行为的时候，有一个方法。可以先大概考虑一下什么是变量、变量决定状态，什么是初始状态、初始值，Next是什么，大概描述一个具体的行为序列，这样可以带来很多启发。刚开始就想得很全面不太可能。

有哪些状态需要描述？i。初始值是什么？0。

接下来写几个序列。i等于0是初始状态，那下一个状态i等于几呢？i可以等于42。再下一个状态i等于几？i等于43。i等于45行吗？不行。i等于43没有了，如何形式化"没有了"后面会讲。这个序列肯定满足行为。

i = 0 -> i = 42 -> i = 43

再写一个序列。i初始值不能等于2，所以i初始值还是等于0。然后i等于41，那么下一个状态i等于42，没有了。

i = 0 -> i = 41 -> i = 42

还可以写很多序列。思考一下，如何用一个公式把这些可能序列全部描述出来？初始状态i=0没问题，Next呢？

写得出来吗？肯定写不出来。第一个序列中i=42后面还有，第二个序列中i=42没有了，逻辑上是矛盾的，既有又没有，所以肯定写不出来。这里隐含了一个控制状态。控制状态不拿出来，是表达不出来这个序列的。状态除了i之外还不够，还有一个pc状态。

3.3.2 Label

脑子里加了3个label：start、middle和done。i的值还跟pc有关。如果pc等于start，i可以等于0到1000任意值。如果pc等于middle，i等于前一个值加1。如果pc等于done，结束。这样你会发现，就能用一个公式把可能序列描述出来了。pc的值是确定的，根据pc的值判断i等于几。

3.3.3 Describing a State Machine with Natural Language

用半自然语言描述如上所示。看似简单的程序里隐含了很多我们看不见的东西，我们脑子里其实有这些状态，只是没有把它说出来，只有出错的时候，你才会考虑pc是不是状态。

这样我们就清楚地把程序的行为用半自然语言描述出来了，完全涵盖了程序的所有行为。打印日志(log)是会漏掉行为的，跑很多次也不全面。

3.3.4 Describing a State Machine with Math

如何用数学来描述？

上面的"and"是自然语言，下面的"/"是数学语言。

pc不带'(prime)就是当前值，这个当前值就是当前状态。pc'是指pc的下一个状态。这是个记法。只要说Si，就是当前状态。

我们说当前值和下一个值，其实在状态描述里引入了时间，我们把时间显式化。这跟Functional Programming有很大区别。Functional Programming是没有时间的，它的函数组合起来可以任意求值。但这里一定要先Si再到Si+1。这是有意选择。如果不这样选择，形式化会非常复杂，而且很难统一纯的Function和有Side-effect的Function。

next value就用prime表达。pc'就是pc的next状态。这也是一种记法，引入符号简化问题。

equals用"="表示。

这样，我们可以将上面的部分翻译成下面的部分。

• 上面是一种简便的写法(松散的表达)，下面就是数学表达了(形式化的表达)，更精确、更准确。
• 再强调一下，这里的if/then/else不是编程语言里的if/then/else。这里是逻辑表达式，是公式。如果if xxx为真，那么逻辑表达式等于then yyy的值，否则等于else zzz的值。状态已经存在了，只是看状态是否满足表达式，是过滤。在编程语言里，如果if xxx为真，那么do then yyy的事情，否则do else zzz的事情。

第一个序列是系统的行为，第二个序列不是系统的行为。

no next values是逻辑表达式，没有什么下一个值了，就是FALSE。

后面会讲，对一个行为来说，什么是FALSE，FALSE代表行为的终止。这里只是暂时的定义，后面会精确地定义终止。

if/then/else变大写了，这是合法的TLA+语法。这就是那个C语言程序的TLA+表达。

大家可能觉得这个好复杂啊，C语言多简单啊。C语言的程序隐含了很多东西是没有显式化的。光一个赋值就要解释很长时间还解释不清楚。大家觉得赋值很简单，其实赋值很复杂，没有大家想得那么简单。但这个公式一目了然，没有隐藏任何东西。

这是完整的数学描述。正常情况下，应该是先写Spec，再写C程序实现。先有个Design Level的描述，然后再有一个编程语言的实现。

可以继续简化一下。TLA+支持结构化的定义。

数学公式可以替换。下面就是完全逻辑变换了。

左上角展开就是右上角。左下角展开就是右下角。

• /和/\的使用。美观、好看。
• 一般会把没有prime的放上面，有prime的放下面。只有没有prime的为真，有prime的才会发生。所以没有prime的一般称为enable条件。这样写是一种比较好的风格。但其实是顺序无关的，完全不是IF/THEN/ELSE。
• i' = i + 1，反过来写，i + 1 = i'，也是对的，因为是逻辑表达式。TLA支持，但TLC不支持。

上面的写法就是下面的意思。

可以用右边的TLA+ Spec来描述左边C程序的行为，而且是一目了然的。

编程语言里是无法表达不确定性的。在我们希望去了解程序的正确性的时候，最大的障碍就是非确定性。我们所说的并发、Side-effect、I/O、分布式其实都是不确定性的呈现。如果不能非常简单、清楚地表达非确定性，是没有办法去形式化地描述系统行为的。TLA+用数学可以非常简单地用统一的形式描述所有的不确定性。精确的描述里蕴含了无限的非确定性。C语言程序里看似确定的描述其实是不确定的。这里可以好好体会一下。并发也是一样，如果写并发程序，跑起来以后行为千差万别，但可以用一个公式精确地表达。一个精确的表达里蕴含了所有的不确定性。这个精确的表达可以进行数学层面的check。

这是数学公式、formula，所以换一下也是对的。

Module Checker是对公式的一种解释(Interpreter)。我们给它一些确定的值，它能够解释这个公式是否正确、满足一些属性。

and满足交换律，但还是推荐左边的写法，不带prime的pc写上面。

如果你的算法是接近代码层面的，可以用PlusCal来写，这样就不用写pc，它会帮你自动生成。如果你的算法很高层的话，也不用写pc。现在写pc是为了更深入地理解TLA+，否则PlusCal生成的代码如果有问题，你很难看得明白。希望大家能够看明白PlusCal生成的TLA+。

Spec大的话，这样写会更清楚一些。写成Pick和Add1，公式更好理解一些。

存盘之后，红色方框处如果是一个绿色的passed就是对的，否则就是有问题的，语法错误。

pretty print。

这是一个公式，是Specification，对应行为的一种描述。我们觉得哪些行为应该是对的，应该满足哪些属性。那如何验证呢？有两种方法。

• 一种是证明，因为是数学公式，可以证明数学公式是对的，但证明代价成本比较高，而且在现实层面因为很复杂也不可行，只能在小范围做，是目前研究层面的热点，因为它的解决能够解决很多问题。TLA+ Toolbox提供了TLA Proof Manager。
• 还有一种叫Model Checker，可以在一个小的空间里生成所有的行为，然后看看是否满足性质，如果满足就是对的，不满足就肯定有错误。Model Checker可以把范围缩小，当然范围是你定的，如果你需要更多的信息，可以把范围搞大点，时间也会长些。因为它是穷举、穷尽的方法。

3.3.5 Model Check

对一个Spec可以有多种Model。对这一种Model可以验证这个属性、范围这样取值。在Model里可以重载一些定义。Int是无穷集，我们把它变成有限集，就0到1000，它就不会穷举所有Int，而只是穷举0到1000。可以在另外的Model里定义成0到100，可以根据不同的情况选择不同的参数。

重点来了。What is the behavior spec?两种选择，一种是Init/Next，另一种是Temporal Formula，后面会讲。现在就选Init/Next，Init填Init，Next填Next。通过Initial Predicate和next-state Relation就可以知道行为是什么了。

选完之后，Run一下看什么效果。报Deadlock。

• Distinct States：在Model Check的过程中，目前一共产生了1011个不同的状态。不一定是1011，可能是1014，跟机器有关。
• States Found：发现了1011个状态，各不相同。什么叫状态一样？两个状态的变量值一样，两个状态就一样。
• Queue Size：产生了但是还没有Check的状态。
• Diameter：直径，连续不重复的状态的个数。S1->S2->S3->S4->S5->S6，但S4=S1、S5=S2、S6=S3，Diameter就等于3。
• Deadlock reached
• Error Trace

这是它产生的一个行为：i=0、pc="start"，i=0、pc="middle"，i=1、pc="done"，结束了没有了。

在"Model Overview"Tab页有一个Deadlock的选项，去勾选，再试一下，不出错了。

在TLA+ Spec里，一个行为默认都是无穷的、无限的，Next是无限的，不可能停止的。如果你想让它停止，必须显式地指定什么叫停止。如果你不指定，它就会Deadlock。这是它的一个特性。在有些情况下，你认为程序是不会终止的，结果Next失效了，它就报Deadlock。这里的Deadlock跟并发编程里的Deadlock概念是不一样的，它只是指一个序列行为终止了而且未指明检查终止条件，你没有告诉我你要check termination，它就报Deadlock。

• Deadlock：如果你没告诉我行为终止但它终止了，我就报Deadlock。如果你不想报Deadlock，去勾选Deadlock就行了。
• Termination：同样是Next没有了，但是你告诉我检查了，那就是Termination。显式地来表达这个问题。
• 对一个行为检查Deadlock，可以认为Deadlock是一个属性——认为这个序列不会终止。之前的序列违反了这个属性，因为它终止了，没有Next。可以认为这是一个最初级的检查，有一个属性Deadlock，有一个Formula，这个Formula的行为违反了Deadlock属性。
• 这个行为符合Spec，但是违反了属性。通过写Spec定义属性然后判断Spec是不是对的。

TLA+里有非常优美的地方在于，什么是一个属性？属性也是一个行为集合。x永远等于3，这是一个属性。这是什么意思？所有的行为里，这个行为的状态序列的状态包含x，如果x永远等于3，那这些行为都属于这个属性。x等于3这个属性代表了所有行为的集合，这个行为是状态序列，如果一个行为的状态序列里的每个状态都包含x变量，并且x变量永远等于3，那么这个行为就属于x等于3这个属性的集合。

一个系统是由一组行为组成的。我们说一个系统满足某个属性，那就是这个系统的所有行为都属于这个属性的集合。x等于3其实是一个行为的集合。我们写一个算法，这个算法也是行为的集合。我们说这个系统满足这个属性，其实就是一个子集的关系。非常优美，这些检查完全可以通过非常简单清楚的逻辑可以表达出来。

Deadlock也一样。所有没有指定Termination而且不会Termination的Behavior的集合就是Deadlock。行为只要不终止就满足，终止了就不满足。现在这个行为终止了，所以不满足。

一切都是行为的集合，一个系统是一组行为的集合，属性也是行为的集合，系统的行为是满足属性的集合的子集(Faye：没说清，系统满足行为集合的子集？)。

3.4 Die Hard Problem

3.4.1 Problem

《虎胆龙威》动作片里有一道逻辑题。有一个人质身上绑了一个炸弹，炸弹上有一个传感器，在很短时间内要求必须放一个正好4加仑的重物它就不爆炸，差一点就爆炸。现在只有一个3加仑、5加仑的容器而且没有刻度，怎么产生一个4加仑的重物呢？

这是剧照。

3.4.2 Behavior

我们要写一个Spec。倒水是个什么问题呢？能不能写一个Spec把倒水的行为表达出来。然后看看如果是需要4加仑，表示什么属性。思考一下，如何把倒水这个行为描述出来。

当你开始写一个Spec最好的方法是写一个行为出来，这里的对不对(correct)不是说刚好4加仑，而是说符合条件。肯定是通过两个瓶子倒来倒去得到4加仑，先不考虑4加仑，先想哪些倒水行为是正确的。

思考：什么是变量？什么是状态？两个桶里有多少水？什么是一步(Step)？假设将水从一个桶倒入另一个桶，可能需要很长时间，但中间状态我并不关心。然后就可以写行为了。可以先在纸上试着写一个可能的状态转换的序列，即Behavior，这个序列不一定要达到最后的4加仑水，合法但不一定正确。

上面是小的、下面是大的。

这个序列可以是无穷的、可以任意倒。我们现在不关心4。

这是一种可能的行为。

3.4.3 Specification

big和small的初始状态均为0。下一步有几种可能性，可以把small充满，也可以把big充满，后面就是把big倒small，也可以把small倒big里，把big倒空，把small倒空，……。那么，一共有几种可能性呢？从Si到Si+1有多少种可能？每个状态下都有6种可能性，只是有的enabled，有的不enabled。

如何用一个公式表达这6种行为呢？其实就是"或"。可以通过"或"来表达这种不确定性。

粗的划分有3种。

细的划分有6种。

FillSmall怎么写？

只写small' = 3就认为big不变了，这是编程语言的语义。在TLA+里不写就意味着任意可能性。如果只写small' = 3，上下两个都是合法的行为，Module Check时会产生下面红框的行为告诉你错了，因为应该是被过滤掉的。必须写一个big不变。这是非常重要的一点，一定要注意，它的影响对于后续Spec组合、Spec之间的实现关系是非常有帮助的，可以简化很多问题。

必须写big' = big，一定要加强。

FillBig、EmptySmall、EmptyBig应该都可以写出来。

EmptyBig少了small不变。

SmallToBig怎么写？

small倒big就是big差多少我就倒多少。

有两种情况，一种情况是big的空间够，全部倒进去。

另一种情况是，big的空间不够，倒一部分进去。

小于等于5说明空间够，如图中THEN分支。如果空间不够呢？

就算还剩多少空间。

都是Formula，可以换。

BigToSmall也是一样。ELSE的第一行写错了，应该是big - (3 - small)。

prime不能出现在"..."处。这是一种风格，否则会很困惑容易引起误解。v'要么等于、要么属于。

• 另外，TLA+定义一定要放在使用前面，放后面会报错。
• EmptySmall只有prime，说明肯定是Enabled。

3.4.4 Model Check

Spec蕴含了很多行为，Model会根据Spec产生满足Spec的所有行为。然后通过属性看一下这些行为是否满足属性。目前属性只有Deadlock。

一个行为是一个状态序列，每个状态就是变化，这个变化就是如何倒水。我们希望存在一个序列，这个序列里存在一个状态，这个状态什么情况下可以满足我们的条件？即Big等于4。

如果正确的情况下，TLC是从来不会告诉你任何情况的，错误的情况下才告诉你错误序列，这个序列违反了。那我如何写一个属性让TLC认为你这个行为违反了这个属性并产生错误序列？这个错误的序列就是我们想要的结果。

存在一个序列，这个序列里存在一个状态，其中Big等于4，是正常的。那违反的话，就是任给一个序列，都不存在一个状态，Big等于4。也就是说，对于Spec所涵盖的所有行为里，每个行为的所有状态Big都不能等于4，如果有答案那肯定违反，一旦有行为违反，Big等于4了，正好是我们想要的。

所以我们现在要写一个Invariant。这个Invariant是个属性。为何叫"不变性"？对于Spec所蕴含的所有行为，每个行为的所有状态里这个属性都为真，我们称之为"Invariant"。Invariant涵盖了所有行为的每个状态下都必须满足的属性。

这里的Invariant就是Big不等于4。我们可以这样来check。

Init和Next还是跟之前一样。

TLA+的Formula可以表达行为，可以表达属性，全部是统一化的。

Deadlock下面有Invariants，点开。

在里面写big /= 4，big没有加prime，就是每个状态的当前值。然后点击"Finish"。

再Run一把，TLC会告诉你"Invariant big /= 4 is violated."，然后产生一个序列，这个序列违反了，这个序列就是我们的答案。

例子虽然小，但都是一些基本的概念，通过小例子更好理解，更复杂系统的做法完全一样。我们的问题在于我们是不是能够深入思考系统的属性是什么，这个东西是没有任何工具可以取代的。TLA+只是提供了一种工具，让你能够比较好地表达思考，但这种思考TLA+并不能给你灌输进去，需要你自己去训练。清晰地思考要做什么，用数学表达出来。

3.4.5 Summary

• x = x + 1永远都是FALSE。
• x' = x + 1当前状态和Next状态满足这个公式。它是关系、Relation、Formula，都是布尔值。

Spec是行为的集合，Property也是行为的集合，我们希望Spec行为集合是Property行为集合的子集。

工作原理：定义Property，行为不满足Property的时候产生序列，这个序列很清楚地告诉我们哪里不满足，很容易看出错误在什么地方。

如果打log的话，首先log不一定能全部展示出来，Bug不一定能复现，即使复现也还得看半天。

3.5 Property

这是一段代码，脑子里把它翻译成状态机。N认为是常量Const。有几个状态：x、y和pc。初始状态x = 0, y = 1, pc = "start"，Next状态x' = x + 1, y' = y * 2, pc = ...。在整个状态序列里，有什么属性可以说呢？有哪些属性是一定要满足的？把x := x + 1; y := y * 2当成一个Step。

• 最终一定会终止，这是一个非常确定的描述。
• 在任何一个状态下，y = 2^x。
• y最终等于256(Faye：应该是1024)。

• 图上有错误，◇后面应该是y，且y最终等于1024。
• □表示y永远是2的x次方，在任何一个状态里，y等于2的x次方。
• ◇表示y最终等于1024。
• 图中的◇x = 256是不成立的属性。

这里是对前面讲的属性稍微扩展一下。

3.6 Invariant and Inductive Invariant

3.6.1 Concepts

这部分的概念非常重要，在理解并发程序的准确性(Faye：正确性？)上至关重要，或者说唯一重要。

在一个行为的状态序列里的每一个状态都保持TRUE的formula就是不变量invariant。

一个formula里肯定有标识符，这些标识符是状态里的变量，这些变量形成一个formula。在任何一个状态里，把变量的值拿出来替换formula的变量都为真。

Invariant表明结果正确。Inductive Invariant表明过程正确。

3.6.2 Euclid's Algorithm

之前是通过数学定义求GCD，这里是通过算法(Euclid's Algorithm，欧几里得算法)求GCD，算法就有步骤了。

• 如果两个数相等，那么它们和它们的GCD相等。
• 如果两个数不相等，肯定一个比另一个大，用大的减小的求差值，然后计算差值和小的GCD。

GCD(M, M) = M
6 6 => 6

GCD(M, N)
6 4
2 4
2 2 => 2

思考如何用TLA+写这个行为。

IF/ELSE和/有什么区别？ 如果A和B是互斥的话，IF/ELSE和/一样；如果不互斥，IF/ELSE其实只能做一个选择，/两个都可以选。

讲这个例子的目的是讲一种一般性的方法：如何证明一个系统是正确的，特别是并发系统。

• 三个变量：x、y、pc。
• Deadlock时pc肯定为Done。
• 序列

x = 6             x = 2             x = 2             x = 2
y = 4          -> y = 4          -> y = 2          -> y = 2
pc = "NotDone"    pc = "NotDone"    pc = "NotDone"    pc = "Done"

思考：这个算法为什么是对的？如何证明这个算法是对的？或者说，如果我们能证明哪个公式，这个算法是对的？精确化一点，如果能用公式证明某种性质，这种性质为真，那么这个算法是对的。我写了算法，对不对我也不知道，并发程序测试用例根本就覆盖不完，靠测试解决并发的Bug是天方夜谭。写个formula出来，证明这个formula为真，那么这个算法为真？这个算法结果对不对？这个算法对不对？

这个算法什么时候结束？pc = "Done"或者x = y。这个算法结束的时候，x、y相等并且GCD(M, N)等于x或y。如果这个公式为真至少可以表明当算法结束的时候这个结果是对的，算法对不对还不知道，结果是对的不代表算法是对的。这是非常重要的概念。

3.6.3 Invariant

图中公式改成下面的，谈的是当前状态，没有prime。

(pc = "Done") => (x = y) /\ (x = GCD(M, N))

pc = "Done"表明算法结束了。pc = "Done"蕴含着x = y且x = GCD(M, N)。这里的GCD可以认为是数学定义的GCD。如果这个公式为真，就表明结果是对的。

这个公式怎么证明呢？

如果一个formula在一个状态序列的每个状态都为真，我们称之为Invariant。看一下前面的序列，这个formula在每一个状态都为真。所以这个formula是一个Invariant。但我们能够证明这个算法是对的吗？

这是一个Invariant，在每个状态都为真，只能表明这个结果是对的。Invariant只能表明这个结果是对的，不能证明算法是对的。可以看到，除了最后一步，前面所有步骤的pc = "Done"都是FALSE，这个公式对步骤没有任何贡献，只有最后一步pc = "Done"是TRUE。

这是一个Invariant，但不是Inductive Invariant。

3.6.4 Inductive Invariant

什么是Inductive Invariant？

F如果是一个序列的Inductive Invariant，首先，在任何可能的InitState中F为TRUE；其次，任给两个状态s和t，如果F在状态s为TRUE，且s和t之间存在NextState为TRUE的，那么F在状态t也为TRUE。我们称F为Inductive Invariant。

像不像数学归纳法？

(pc = "Done") => (x = y) /\ (x = GCD(M, N))这个公式是不是Inductive Invariant？

• 首先，在初始状态下为真，成立吗？成立。
• 任给两个状态s和t，如果这两个状态满足NextState的情况下，那么如果F在s为真，它在t一定为真，成立吗？

x = 6             x = 2             x = 2             x = 2
y = 4          -> y = 4          -> y = 2          -> y = 2
pc = "NotDone"    pc = "NotDone"    pc = "NotDone"    pc = "Done"

举个例子。在上面的序列中，状态sx = 2, y = 4, pc = "NotDone"，状态tx = 2, y = 2, pc = "NotDone"，这两个状态满足NextState(肯定满足，因为这是一个正确的序列)，公式在状态s为真，在状态t也为真，那就是说，对于这个序列来讲，用我们选的两个状态，公式都为真。但这不说明问题。因为这是一个正确的序列，我从这里选的两个状态，肯定满足。但定义中是any Si和Si+1，任给两个状态。我可以构造两个假状态，这两个假状态是满足NextState的，但公式不成立。

如果pc = "Done"对前面的步骤没贡献，让它贡献一下可能就出错了。

初值 x = M, y = N

     s------Next------>t
x    6                 6
y    6                 6
pc NotDone            Done

s和t满足NextState，但这时pc等于"Done"了，x也等于y了，但是GCD(M, N)是不是等于6呢？不一定，M和N可以任意改的，比如M为8、N为6，GCD为2。F在状态s为真，在状态t为假。

这就是定义。这样根据数学归纳法就可以证明这个算法是正确的，Inductive Invariant比Invariant条件更强。找到Inductive Invariant和Invariant，证明Inductive Invariant蕴含Invariant，就可以证明不但结果正确并且过程也是正确的。Invariant断言结果，Inductive Invariant还断言了迁移，将过程和结果之间的关系建立起来，过程对结果对，过程不对无所谓结果对不对。本来我说1加1等于2，你告诉我3减1也等于2，但我需要1加1。这也是算法和函数的区别，函数只关心结果，但算法一定要关心过程。因为大部分设计都是算法，不是函数，一定要注意本质的区别。

图中的prime都去掉，(pc = "Done") => (x = y) /\ (x = GCD(M, N))。

图中的公式，就是当程序终止的时候结果正确。当pc = "Done"，程序终止了，结果(x = y) /\ (x = GCD(M, N))是正确的。在TLA+里，这样的定义，我们通常称之为"PartialCorrectness"。这个词的意思是：如果你的程序终止的时候它的结果正确，这个属性叫"PartialCorrectness"。但这不能表明算法正确。

什么叫算法正确？I3。我们要把Inductive Invariant找出来，这个Inductive Invariant蕴含PartialCorrectness，才能证明，结果是对的并且过程也是对的。这是非常重要的性质，PartialCorrectness是结果，Inductive Invariant是过程，如果过程蕴含结果，那么这个过程就是对的。

我们不能只看结果，结果靠不住，我们测试测的是结果，可能依然会蕴含非常多的错误。特别是在并发程序里，找到Inductive Invariant决定了是不是真正理解了这个并发程序。

整个体系是，通过Inductive Invariant表明过程里面的不变性，如果过程里面的不变性蕴含了结果正确，证明这个算法肯定是对的。找出Inductive Invariant是你对算法是否理解的本质表现，而且是唯一有效的寻找并发程序那些微妙错误的手段。

那么，什么是GCD的Inductive Invariant？ 原因是pc = "Done"对前面的步骤没有任何贡献，所以前面随便乱写，结果还是对的。所以要让它有所贡献。在这种情况下，我们希望每一步都是正确的，不能随便改，即GCD(x, y) = GCD(M, N)，每一步x和y的变化都不能把GCD(x, y)变成另一个值，那我永远回不去了。假设其中某一步，GCD(x, y)不等于GCD(M, N)了，后面发现又相等了，那肯定有问题了，因为这一步一旦不对，因为就两个信息，没别的信息了，后面即便对了，也是负负得正凑出来的。现在限定了，每一步x和y的变化都要满足GCD(x, y) = GCD(M, N)。一旦加上这个限定，前面的反例就不成立了。

在找Invariant的过程中，TLC可以帮助我们做很多工作，可以先试探性地写一些属性，把这些关系教给它去检查，它不报错，你就知道是对的，知道一件事情是对的再去想它为啥是对的比不知道对错去想要容易得多。这是一个非常重要的经验，Lamport经常这么干。

Inductive Invariant怎么写呢？要满足I1、I2和I3。

• GCD(x, y) = GCD(M, N)并且pc = "Done"、那么x = y。
• GCD(x, y) = GCD(M, N)为什么是对的？要证明在每个状态GCD(x, y) = GCD(M, N)都是对的。这是第一步。还要证明Inv是否蕴含PartialCorrectness。
• 要证明GCD(x, y) = GCD(M, N)是对的，有三个定理需要证明，不展开讲了。这三个定理证明完之后，并且证明Inv蕴含PartialCorrectness，我们才能证明Inv是Inductive Invariant。
  • 任给m属于自然数且不等于0，GCD(m, m) = m，显而易见。
  • 任给m属于自然数且不等于0，GCD(m, n) = GCD(n, m)。
  • 任给m属于自然数且不等于0，如果n > m，那么GCD(m, n) = GCD(m, n - m)。

证明一个算法的正确性并不是那么简单。这只是一个顺序程序。在现实中，我们只要证明我们所关注的算法的正确性即可，证明过的定理可以认为是正确的，拿来就可以用。

如果这三个定理都为真，来看看Inv是否正确：

• 初始情况下，x = M, y = N，GCD(x, y) = GCD(M, N)为真；pc不等于"Done"，pc = "Done"为FALSE，pc = "Done" => (x = y)为TRUE。Inv为真。
• 如果Inv在状态s为真，在状态t是否为真呢？定理3可以证明GCD(x, y) = GCD(M, N)为真；如果pc不等于"Done"，pc = "Done"为FALSE，pc = "Done" => (x = y)为TRUE；如果pc等于"Done"，pc = "Done"为TRUE，x = y，pc = "Done" => (x = y)为TRUE。Inv为真。
• Inv是否蕴含PartialCorrectness，即(pc = "Done") => (x = y) /\ (x = GCD(M, N))？如果Inv为真，(pc = "Done") => (x = y) /\ (x = GCD(M, N))也要为真，为真吗？为真。长公式做个真值表就可以判断了。

每个算法的Inductive Invariant都不一样，而且基于正确性的不同，可能找到不同的Inductive Invariant。

3.6.5 Lamport Papers

Erik Meijer是非常著名的Functional专家。这是channel9对Lamport的采访。Lamport是并发的权威，全世界没有人比他更理解并发。

在采访中，Lamport说，他感觉很多人都在数学里寻找银弹(magic bullet)。如果能够找到一种正确的数学，那么数学就能帮你解决问题。但事实并非如此。当你理解了某个东西的时候，你才能找到数学去表达这个东西。数学并不能给你提供这种理解。

很多人都会用规格说明和验证方法解决同样的问题，Lamport也是这样。这些人都会想去寻找新的数学抽象，Lamport找了20年放弃了。Lamport发现，举个例子，如果想证明并发算法的正确性，有一个非常基本的、肯定有效的方法——证明一个Invariant，但这个Invariant其实是Inductive Invariant。不管你怎么鼓捣、怎么包装一些方法，不可能让你的证明更简单。通过方法的变换让证明更简单是不可能的。证明的固有复杂性是存在的，不可能再降低了，通过变换方法降低复杂性是不可能的，到一定层面就不会再降低了。Lamport采用的方法很简单，就是尽可能直接地从问题到数学，这件事情对他来说很容易，因为Lamport本来就是用数学来表达算法的，它已经是数学了，而且不需要任何额外的语义了。其他的所有编程语言，都是用编程语言去描述问题，然后再赋予编程语言语义，这个语义一般是数学，多了一层，而Lamport是直接把问题变成数学，已经有语义了，并不需要再去寻找其他语义了。其他人需要重新去把对算法的描述用语言转换成数学，Lamport不需要，Lamport不需要再去鼓捣那些稀奇古怪、各种各样的数学让翻译过程变得平滑，搞得更复杂。

事后Lamport知道，这些人最终会发现所有这些新的数学方法其实不能真正地解决问题。可以看到并发程序里Invariant的重要性。你的算法、你的并发程序理解了，你就要把Invariant写出来，Inductive Invariant写出来，写不出来是有问题的。第一天讲的那么简单的并发程序，能不能把Inductive Invariant写出来？如果写不出来，怎么指望能理解更复杂的程序呢。

这是另外一篇论文，是Lamport在1977年写的，证明并发程序的正确性。学并发编程，精华全在这些论文里，学语言只是学了皮毛，根本不理解并发。

在70年代中期，有些人都在思考问题：如何验证并发程序的正确性。Ashcroft写的一篇基础论文《Proving Assertion About Parallel Programs》，发表在1975年的杂志上。这篇论文第一次引入了invariance(不变性)的基本概念，用不变性验证并行程序的正确性。Lamport发现用这个思想能够把验证并发程序的Floyd方法更一般化。事后来看的话，他的想法现在看很明显，但当时没有。好方法一般都这样，没出来的时候大家都不知道，出来后大家都觉得就应该这样。但其实，花了Lamport很长时间才得到这个想法，但我一提出来，大家觉得这个想法很明显。我记得有个时刻，我想需要一个证明，对于一组处理进行归纳，其实就是Inductive Invariant的雏形。

当我们开发我们的方法时，Owicki和Lamport还有很多人都想对Ashcroft的想法进行改进，因为Ashcroft的想法是一个全局assertion，他考虑到我可以用pc状态对整个程序做全局的断言。他们觉得Ashcroft的方法很落后，认为Owicki-Gries方法是一个巨大的改进，因为它使用了程序文本对证明进行分解，把一个大的Proof分解成小的Proof。大家觉得如果分解开更好。后面发现这是错误的。最后是写一个global invariant。编程语言都提供annotation标注，一定程度上可以让你在编程语言层面上打标注来约定一些property。把invariant写成一个annotation允许你隐藏一些不变性对于控制状态的显式依赖。如果我用annotation写属性，从编程语言我看不见pc状态了。但是，你把算法写成一个程序，把不变性写成annotation而不是一个全局的不变性，让事情更复杂。很多情况下，通过pc状态更容易写出更清楚的不变性，因为程序的正确性依赖pc状态。更糟糕的是，通过编程语言写annotation的话，会让你把一整块的东西分成一些独立的断言而不是一个全局不变性。然而global invariant是最重要的。Lamport认为，一个程序的正确性一定是全局的，不能拆开。Lamport认为Ashcroft是对的，他们三个搞砸了，花了他们好长时间才发现这个问题。

Annotation有用，但如果想用处越来越大，就会越来越复杂。

3.7 Reference

到此，TLA+静态部分就讲完了，不需要时态逻辑。大部分的系统用我们目前讲的内容就可以写Spec了，完全没有任何问题。目前讲的都是如何check正确性。只要写Init和Next、加上Property完全可以解决90%以上的问题。

后面的TLA部分，理解这些概念对于理解动态系统会有很大的帮助。