• 1 Introduction to Course
  • 1.1 Computer "SCIENCE"
  • 1.2 Leslie Lamport
  • 1.3 CORRECTNESS
  • 1.4 The Art of Debugging
  • 1.5 Alan Turing
  • 1.6 Robert Floyd & Tony Hoare
  • 1.7 Lamport, 1977
  • 1.8 Amir Pnueli, Temporal Logic, 1977
  • 1.9 TLA (Temporal Logic of Action), 1994
  • 1.10 Examples of TLA+ Application
    • 1.10.1 Use of Formal Methods at Amazon Web Services
    • 1.10.2 A real-time operating system designed using TLA+
    • 1.10.3 Cosmos DB
    • 1.10.4 Good Response about TLA+
  • 1.11 CORRECTNESS Driven Design
    • 1.11.1 Insertion Sort
    • 1.11.2 Coffee Can Problem
    • 1.11.3 Teaching Concurrency
  • 1.12 Summary
  • 1.13 What is a COMPUTATION?
    • 1.13.1 Computation and State Machines
    • 1.13.2 Computation
    • 1.13.3 Whorfian syndrome
    • 1.13.4 State Machine
    • 1.13.5 Specifying a State Machine
    • 1.13.6 An Example (Factorial)
    • 1.13.7 State Machines in Action (Two Programs)
      • 1.13.7.1 Program X
      • 1.13.7.2 Program Y
      • 1.13.7.3 Program X & Program Y
    • 1.13.8 Abstraction/Implementation
  • 1.14 State Machines (Lamport's two classic papers)
  • 1.15 Lamport's sayings
  • 1.16 Reference
  • 1.17 Faye's Summary

天生对数学有一种恐惧，觉得数学难、没用、距离实际工作比较远？Lamport在很多场合采访中经常吐槽数学的教育，尤其在计算机科学领域，认为计算机科学领域的数学教育做得太糟糕了，如果做得好一点，整个计算机系统的可理解性会更高。

先来讲讲“computer science”。“SCIENCE(科学)”这个词，大家肯定会认为这是一个褒义词，崇尚“科学”，但“科学”的历程远远没有想象中那么美好。

每一次科学的进步，都可能有人会付出惨痛的代价，并以此为驱动。因为每一次科学的进步会引起当前社会里权利、利益财富的再分配。一方面，当权者或者利益运维者会阻碍科学的发展，让大家了解真相的话，就没有办法垄断他们已有的利益。另一方面，就我们个体而言，对科学的接受也是一个比较痛苦的过程。几万年以来，大部分情况下，人类跟动物是没有区别的，生活资源比较匮乏，到处充满了危险。能在衣食无忧的情况下有时间做理性思考也就是最近几百年的事情，最近一个世纪是比较密集的。我们的大脑对于整个科学的接受存在一个冲突。人的大脑分为两部分，一部分是动物大脑，之前人类在野外生存的时候，物质匮乏充满危险，接受科学知识需要深入、理性的思考，必须把逻辑关系想清楚了才知道这是合理的，但这种思考是非常消耗能量的。你正在思考的时候，动物大脑会提出反对，太耗能量了停止思考吧，要把能量保存下来，以适应野外生存。另一部分是理性大脑，理性大脑在思考的时候，会被动物大脑打断。所以说，对于个体来讲，接受科学是非常困难的，这是人类大脑结构的进化跟不上目前科学的发展造成的结果。

布鲁诺因为日心说被烧死。当时的宗教并不是不知道地球不是中心，只是如果承认的话，他们的权威就会被打破，所以会阻碍日心说的流行。

但是，人类大脑还有一个比较独特的地方：我们有元认知能力，我们知道我们在想什么。大部分情况下，元认知能力都是被压抑的，没有得到充分利用。我们在思考一个问题的时候，我们的动物大脑说：“停下来，不要想了，因为食物匮乏，这会消耗太多能量。”，这时我们的元认知会告诉我们：“旁边的冰箱里有食物，不用怕。”。通过元认知能力的调动，经过几万年进化的动物大脑会被压制。如果我们有意识地做这些训练，元认知能力会被慢慢唤醒，可以长时间理性思考，理性思考会带来非常深远的成就感和愉悦感。

我们的工作也是一样的。我们在设计系统的时候，有机械动作和清晰思考。清晰思考可能被压抑住了，要通过训练把清晰思考调动起来，我们思考清楚了，我们设计的系统自然就好理解多了。

这个课程的核心TLA+是Leslie Lamport发明的。Leslie Lamport目前是微软首席研究员，2013年获得图灵奖。云计算、云平台最核心的部分都是基于他的两篇论文，一篇是关于事件时间顺序，一篇是Paxos算法(容错、数据一致性)。Lamport是一位应用数学家，但他的研究领域则是在计算机科学领域。他有一个特点，不像其他学者，他的研究课题都来自于软件工业里的实际问题。一个实际的问题，经过他的思考，把问题的细节剥掉，把最本质的地方拿出来，来做研究。他自己也说，我并不是说对这个问题能给出多么好的解决方案，而是说我能识别出最好的问题。这得益于他的清晰思考，他一直把他的这种能力归结于自己能够长时间地深入地做清晰思考。这也是为什么他的文章即使过了四十年、五十年，完全不过时的原因。他能够剥掉问题纷繁的细节得到最本质的东西呈现出来。

http://lamport.azurewebsites.net/pubs/pubs.html

这个网站列出了Leslie Lamport的所有论文(180+)。他的论文每一篇都是精品。他的写作有一个特点，他的文章高中生就能看懂，但博士生也能从中受益，非常清晰流畅，可以作为写作范本。而且随着你的成长，可以重复去看，随着你经验的丰富，看出来的东西越来越多。

孙鸣老师推荐首先阅读其中的两篇论文：

• Computation and State Machines
  http://lamport.azurewebsites.net/pubs/state-machine.pdf
• The Temporal Logic of Actions
  http://lamport.azurewebsites.net/pubs/lamport-actions.pdf

本课程的内容就是从这些论文里提炼出来的。

本课程的内容是关于“正确性”的。

软件行业发展迅猛，各种各样的技术、语言和方法蓬勃发展，还有各种系统设计。也有很多会议分享，有可伸缩性、容错、性能、高可用性等，但你会发现很少有分享“正确性”的。在写设计文档时，文档模板中有很多项目，我们会写去掉状态(无状态)可提升伸缩性，数据复制策略可保证可用性，用错误重试策略做不同的可用性的组合，把某个点消除掉提升并发性能，在资源单点用无锁的方法提升性能，会有很多这样的设计在文档里。唯独“正确性”这一节怎么写呢？

有些系统，本身很复杂，例如编译器，但即使再复杂，它就是一个函数，输入输出是确定的。但有些系统，本身很简单，比如时钟Tick、Tick、Tick ……，每秒钟Tick一次，但却无法用一个纯函数表达。如果一个系统能用一个纯函数表达，就可以用一些目前已有的数学理论推导来做，况且还有涉及I/O的、Reactive、并发、分布式等系统，是完全没有办法用纯函数表达的。大部分系统都是无法用纯函数表达的，能用纯函数表达的系统，要么是一个小模块，要么是一个类似编译器的独立的系统。那么，这些无法用纯函数表达的系统怎么来写正确性呢？

正确性是基础。没有正确性，其他都是零。

为了保证正确性，我们会做如下工作：

• Design Review
• Code Review
• Simple Design
• Test
• ... ...

Design Review，设计完了之后，找同行来看一下是否有问题。Code Review，实现出来之后，找同行来看一下是否有问题，代码是最精确的。强调简单设计，因为设计简单的话，容易看出来错误。复杂性有两种：固有复杂性和偶然复杂性，固有复杂性是问题本身内在的，偶然复杂性是开发工具、开发方法和设计方法引入的。通过简单的设计尽量减少偶然复杂性，减少问题。再来说测试，可以把系统当成一个黑箱，它很像一个贝叶斯模型。假设系统中有很多点是独立分布的，测试点测试通过越多，正确率越高。单纯从黑箱来看，测试其实这样一件事情。

但从设计软件系统来讲，它的正确性并不是一个概率问题。越是重要的系统，我们越是希望它百分之百正确，否则一旦出问题代价非常高。而光靠测试是达不到这个效果的。最终还是要在设计系统的时候，知道它是正确的，那么如何知道它是否正确呢？

简单设计亦是如此。怎么知道“简单”不会引入错误？举个例子，把某个条件简化一下，这样简单，但简化完之后会有什么后果呢？首先应该有一个正确性的保证，然后才能做简单设计。假设我们知道如何做正确的设计或者知道如何把握设计的正确性，只有在这个前提下，我们才能说可以做一些简化后，还是正确的并且简单。盲目简化，特别是对于并发系统，是一场灾难。

Foundation of Software Engineering
现在的软件工程看起来很热闹，各种方法和语言层出不穷，但软件工程的基础是正确性。正确性方面一个微小的进步就可以为整个软件开发带来巨大的推进。可以看到，在软件正确性方面的理论层面的一点进步，就会出来很多图灵奖得主。

本课程不讲设计方法，而是讲如何做正确性的设计。或者说，如何用科学的方法表达出你希望系统做什么东西。需求文档和UseCases都是不正式的，因为没有办法证明系统是否按期望运行，没法检查。

On the Proof of Correctness of a Calendar Program
http://lamport.azurewebsites.net/pubs/calendar.pdf

这篇论文是Lamport在1979年写的，证明一个日历程序的正确性。很多编程语言编程方法被鼓吹得怎么好怎么好，感觉好像这些方法能够自动产生好的程序。其实不然。有一个算法设计，如何对它进行推导推理，证明它是正确的？这些方法是做不到的。“结构化编程”也不会让欧几里得发现他的算法。Lamport并不是否认这些方法，软件工程有很多维度，软件正确性或者说如何表达软件系统想干什么跟如何更加清晰地组织代码、更加高效地组织团队是正交的，是两件事情，不能混为一谈。好的设计方法、好的语言是不是能提高正确性呢？其实两者并没有本质的联系。

【Faye】But，我在这篇论文里并未找到这段话？

关于正确性，我们其实很少正式地去思考这个问题，做一些Design Review、Code Review和测试来保证。但是如果系统已经开始运行，出问题了怎么办？最有效的方法是调试(Debug)。调试工具的强大是我们喜欢的，那我们是怎么调试的呢？对这个问题的深入思考，可以得到本课程主题的框架。

看哪里出错了，想一想，先有一个猜测。这个猜测并不是猜测，是你对系统行为的一种期望。举个例子，x变量的值应该永远是3；如果执行到这条语句，那么下条语句一定要执行到，否则就是Bug；假设一个并发系统，如果程序要进入到临界区了，那么它一定要进入到临界区，否则就是死锁、出错了。我们会有一些期望，这些期望是基于我们设计的系统的行为做出来的，跟实例化无关，不管是用C/C++、Erlang或是Haskell语言写，不管是用面向对象还是函数式，这是问题本身内在蕴含的。

图中右上角是基于我们对系统的理解提炼的一些属性(Property)。举个例子，某个变量x，x永远等于3；假设程序进入到某一行(Label X)，那么它一定执行到另外一行(Label Y)，跟日志打印是一样的，before xxx line...，这也是一种属性。我们可以基于对业务朴素的理解提炼很多属性，现在是放在我们脑子里的。

图中下方是我们的程序(Program)。系统跑起来以后，加断点调试，但断点肯定也不是随便加的，不会所有地方都加断点。图中虚线表示程序的执行序列，运行的程序是一个离散系统，但“步”非常小，断点加上以后是大“步”。图中○表示断点，每个断点断下来以后，看到的是系统的状态，变量很多，但肯定不是所有的变量全看，假设是变量x、y、z...，还有一些是程序里没有的，例如Call Stack。我们基于对业务的理解，关注这些状态和特点。

图中上方是我们脑子里认为的东西，先不起名字，只关心x和y，z觉得没用、不看。

在Program部分的执行序列上采样状态快照S1(x、y、z...Call Stack)、S2(x、y、z...Call Stack) ……，在Brain部分也对应有状态快照S1(x、y)、S2(x、y) ……。在每个点上都会提炼出来一个东西，Program部分S1到S2是一个变化，Brain部分S1到S2也是一个变化。基于Brain部分中的判断，根据Program部分的值，看是否有问题，如果Program部分的值不满足Brain部分的判断，就可以定位出来哪里出了问题。这就是我们平时的调试方法。

但并发程序加断点是没有用的，因为一加断点，race condition就没有了，结果就不出现了。那么就加日志，日志也不是随便加的，肯定也是找点，跟断点无本质区别，断点会把程序停下来，日志也是把程序停下来，只是对于并发程序来说，日志一般不影响原来每个步骤之间的交错顺序，可能不会影响到race condition，问题可以复现。

并发程序很难调试，因为问题不是那么容易出现。可能这次CPU跑得慢，问题不出现；可能这次CPU跑得快，问题出现等。但顺序调试和并发调试并没有本质区别。后面会讲到，并发的本质是什么。

图中的Program部分是“实现(Implementation)”，写出代码，里面涵盖了各种各样复杂的状态，包括程序里有的x、y、z和程序里没有的Call Stack，状态快照S1、S2、S3……是系统实现的。Brain部分是我们脑子里的东西，称之为“抽象(Abstract)”，在理解程序正确性的时候，并不一定要关心所有细节，关心这个错误所涉及的状态信息，状态快照S1、S2、S3……是脑子抽象的。Brain部分的S1、S2、S3……序列代表了系统的行为，我脑子里其实是有一个我觉得系统应该干什么事情的东西的，只是说我把它全放到代码里去了，但出问题的时候，强迫我反向把它搞出来。那我如何知道有没有问题或有没有违反什么东西呢？我必须知道Property，必须知道本来期望它要满足什么性质。

形式化方法(Formal Method)的核心就是这个框架，只是说如何形式化。上图中Property的写法是很含糊的、手工的。如何形式化正式地描述呢？什么是x always等于3？什么是执行了Label X一定要执行Label Y呢？这些都是脑子里的描述，如何形式化表达出这些概念呢？同理，如何形式化表达Brain部分的状态、状态之间的关系(S1怎么到S2)？

编程语言也是一种形式化，但它的目标是产生高效的代码，并不是为了让你验证程序的正确性，所以它很复杂。如果想要验证程序的正确性，可以用别的方法，并不一定要用编程语言这么复杂的方法。这里的选择很多，如何定义Property和Abstract决定了很多不同形式化方法的不同道路。还有一个关键点在于，Abstract是一个简化，如果我发现Abstract违反了Property，那么如何可以肯定Implementation一定有同样的问题呢，因为Implementation要复杂得多。Abstract和Implementation之间是蕴含(Imply)关系(Implementation => Abstract)，如果Property中关于x、y的论断在Abstract中是正确的，那么在Implementation中一定是正确的。

这是一个框架。首先，希望通过一套方法把系统的行为通过状态序列描述出来，状态序列中的状态是提炼出来的，不是所有的，甚至可能包含pc、Call Stack等这些程序中看不见的状态，但很多Bug是隐藏在这些状态中的，不通过这些状态的验证，很难知道问题出在哪里，光看代码是看不出来的。然后，希望有一种方法表达这些状态、迁移、属性，而且能够做到Abstract的问题一定是Implementation的问题(保证蕴含关系)，否则发现Abstract有问题但Implementation没问题，就白做了。所有形式化的方法都是解决这个问题，TLA解决得非常优雅。基于这样的认识，并发和非并发就没有区别了。很多形式化方法在解决一个顺序程序问题时做得非常好，但一遇到并发程序就不行了，没法表述了，要换一套方法来解决，TLA则不然，后面会讲到。

上图就是Debug的一个形式化，里面有一些严格的关系，非常重要，要时刻放在心里。

An Early Program Proof by Alan Turing https://pdfs.semanticscholar.org/dfd7/34b2de2cbcce6ac07e909011b0ed6ba32b01.pdf

Alan Turing在很早以前就写了一篇论文《Checking a Large Routine》，如何检查一个大的例程(Routine)，可以认为是一个过程(Procedure)。如何能够从正确性的方面来检查一个例程呢？一个人去检查例程，为了让他的工作不那么困难，程序员应该定义一些assertion(本质上是对属性的断言)，这些assertion可以单独check，这些assertion合在一起形成了对于正确性的支撑，这些assertion都对就肯定是对的。这样验证程序就会简单很多。这篇论文写得很早，而且思想性很深远，却没有引起任何反响。

计算机科学有两派：计算派和语言派。Alan Turing发明了图灵机，是计算派的创始人，另一个计算派创始人是发明了Lambda Calculus的丘奇。

这篇论文之所以没有广泛流行，是因为Alan Turing在写这篇论文的时候数字都是反着写的，1234写成4321，看起来头疼。Alan Turing早期编程的机器叫Manchester Machine，这个计算机的数字表示全是反的，他很习惯了。

受这篇论文影响的两个人物：Robert Floyd和Tony Hoare，也是两位图灵奖得主。他们是语言学派的，在Turing的思想上发明了Floyed Hoare Logic，用这个逻辑来表达Turing的思想，也因此获得图灵奖，但这不是我们的主题。GO语言的CST模型也是Hoare提出来的。

Lamport是1970年开始进入形式化领域的，刚开始跟随Robert Floyd和Tony Hoare，但后面出现了分歧。在分歧之前，他写了一篇文章给ACM杂志。

大意是说：数学家在发表论文的时候肯定不会说这是我的猜想，光漂亮没用，一定要证明出来为什么是对的。程序写出来根本就不提这回事，只谈设计多么优美，这么来说，程序只是一个猜想，程序不能保证正确性。他非常认可程序一定要检查正确性。

后来出现了分岔，Lamport选择了一条跟Floyd和Hoare完全不同的道路。

分岔还是源于两派：语言派和计算派。Floyd和Hoare发明的Floyd Hoare Logic是基于语言的，语言能描述的东西我才能看得见，如果语言不能描述，这个东西不存在。编程语言里其实没有Call Stack，那这个形式化方法就不存在。好处在于解决问题会非常漂亮，坏处在于会增加很多困难。如果不让看Call Stack，直接形式化推演错误，是非常痛苦的，非常复杂。Lamport是个务实派，他一直在解决工业问题，他觉得不要拘泥于这些东西，关注计算层面的概念，这个概念只要存在就拿过来用，如果它能让自动化验证简单的话就更要用，因为这个事情本来就很难，如果选一个为了解决这个问题而增加难度的方法，得不偿失。

这是一个非常重要的区别。从语言层面的视角，程序的Control State、Call Stack、pc指针语言里没有，就不存在、不能看到，但从计算层面的视角，如果让Control State等能够显式化，那么可以把并发程序、分布式程序、批处理程序、I/O 、Reactive全部统一在一个简单框架里。

如果没有Control State、Call Stack、pc指针，但正确性还依赖于它们，又没有显示化表达，就只能通过复杂的观察者去看它们，观察它们的反应推断一个东西，这会带来很大的复杂性。

Lamport说：

• The fundamental problem facing computer engineers is complexity.
• Good engineering means making systems as simple as possible.
• The math needed to describe computer systems is simple.
• Programming languages are complicated.
• You don't achieve simplicity by thinking in terms of complicated languages.

如果所选择的描述系统的语言很复杂，肯定不会简单。因为不可能用一个复杂的东西去描述一个很简单的东西，肯定搞复杂了。Lamport认为数学(小学数学、高中的初等代数、本科离散数学、逻辑、集合论等)很简单，编程语言很复杂。走语言派是很困难的，但如果做成，可以做end-to-end的验证，可以从最高层的规格说明到最低层的code统一验证，因此很有吸引力。但Lamport认为，首先这在目前是不现实的，而且目前必要性也不大，因为如果能在高层把算法验证好就已经很好了。他做了一个权衡，牺牲了end-to-end的验证。而且“高层”可以选的，可以把状态降到CPU、寄存器层面，也可以放到很高的算法、高层的系统设计层面，并不是说，只能做高层，不能做低层。一个真实的系统，用编程语言写完程序后，可以compile成机器代码，做end-to-end的验证，他没有选择这条道路，这也是TLA+伸缩性比较好的原因，没有编程语言复杂，而且可以统一各类系统，不管是并发的、分布式的、Reactive的、I/O、有无副作用的，完全都一样，都可以用同样的公式，只是不同的解释。后面会讲到并发跟顺序没有任何本质区别。

TLA的TL是Temporal Logic(时态逻辑)。Amir Pnueli在1977年发明了Temporal Logic，为Lamport开创了一条新的道路。

Lamport一直觉得没有必要为了解决问题的工具的正确性而增加额外的复杂性。问题在那儿，解决问题的工具很复杂，忘了问题，这是不对的。但Temporal Logic也很复杂。Lamport一直希望开发一种方法能够给一线程序员使用，Temporal Logic是很难理解的，所以他在这个基础上抛掉Temporal Logic的很多东西。如果仅仅只是想解决Abstract层面的正确性问题，而不考虑Abstract和Implementation之间的直接翻译(但正确性的属性是可以映射的)，那么可以对Temporal Logic做很大的简化，所以Lamport做了TLA，A是Action，用TLA来描述Abstract层面，同样描述Property。这也是TLA的优点。Abstract部分可以认为是设计的行为描述本身，对行为的描述跟对行为的属性的描述是一样的，而且从高层到低层都可以用TLA描述，它们之间的蕴含关系就是逻辑推导关系，统一到一个框架里。

TLA+的Plus是什么意思？每个状态S都有x、y状态，这些称为TLA的静态部分。TLA本身是描述行为，是动态的，每个点上都有一个状态，TLA对这些状态如何定义是不管的，怎么定义都行。Plus是指如何描述静态状态。Lamport在TLA+里选择集合论和一阶逻辑来描述静态状态。

The Temporal Logic of Actions
http://lamport.azurewebsites.net/pubs/lamport-actions.pdf

Lamport于1970年进入形式化领域，1977年开始接触Temporal Logic，到1994年写了《Temporal Logic of Action》论文。Lamport写了两篇TLA的论文，第一篇写完后，过了几年又写了一篇，说第一篇搞错了，现在彻底搞懂了再写一篇。这篇论文写得非常好，建议精读。如果想彻底理解并发控制系统的话，这篇论文是必读的。

Temporal Logic of Action (TLA)是一个逻辑框架，用来描述和推导并发系统，分布式等其他系统也是一样的。用同样的逻辑来表达系统和系统的属性。Debug图中的Abstact部分和Implementation部分都是系统，Property是属性。对系统是否满足一个属性的断言等同于一个系统实现了另外一个系统的断言，后面会举例子。

TLA的语法和语义都很简单，一页纸可以搞定。但TLA并不是逻辑学家的玩具，它非常强大，而且在工业里确实是可以用的，证明它是有实际用途的。

他认为Temporal Logic太复杂，他有同事为了使用Temporal Logic描述一个FIFO的队列，描述了两页纸，完全不能用。现在描述一个FIFO的队列只要几行。Temporal formula时态公式比普通的一阶逻辑要难理解得多，而且对它的推演非常困难。能把逻辑学好是非常困难的，逻辑一不留神就出错，而且错误非常微妙。要选择简单的语言——数学，数学里最简单的就是集合论和一阶逻辑，这样保证推演没什么问题，这样来描述复杂性真的可以做到简单。

这是Lamport的哲学选择，elegance不是我们追求的核心目标(语言派追求elegance)，而是以真实世界算法问题的需要来作为驱动力。严格推理是唯一避免微妙错误的手段。我们想让推理通过底层形式化的手段变得非常简单。

Temporal Logic很复杂，要规避掉，Lamport加了A，A封装了很多细节，不用关心。初衷是解决实际问题，让形式化尽量简单，这样推理也简单了，也实用化。

Use of Formal Methods at Amazon Web Services
http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf

这是TLA在工业中的应用实例。第一次在公众视野里出现的大规模应用TLA的企业是亚马逊，源于亚马逊的一篇论文。亚马逊是做云服务的，里面有很多基础设施，并发的分布式系统，非常复杂。系统复杂到如果不用形式化方法质量难以保证，而且重启的代价非常高。亚马逊花了很长时间去找这种方法，后来发现了TLA，非常成功。

大部分formal method确实很难，只有逻辑学家和数学家才能看懂，而且只能解决很小的一部分问题，没有伸缩性。但TLA+可以描述整个系统，可以把整个Amazon的Dynamo机器全部描述出来，也可以描述Paxos算法或者一个很小的Euclid算法。

在对正确性有把握的情况下，可以大胆优化，只要正确性没有被破坏。代码其实很难改，代码改本身很容易，但代码改了不出错是很难的。如果把正确性当作第一位的话，视角完全不一样。

上图是媒体的报道，亚马逊通过这种方法极大地提升了的质量、性能和效率，keep up if you can!

The previous version flew on the Rosetta spacecraft

欧洲航天局有一个实时操作系统，原来用C语言写的，后来的新版本里用了TLA+，用TLA+定义Spec，系统做了大量简化，代码量减少了10倍，而且更清楚，更容易保证正确性。写了本书，这本书里专门讲了这个方法。

The TLA+ abstraction helped a lot in coming to a much clean architecture.

One of the results was that the code size is about 10x less than the previous version.

引文中提到的“抽象”跟我们平时所说的抽象完全不一样，不是一个维度。引文中提到的“抽象”主要是基于正确性的。

https://techcrunch.com/2017/05/10/with-cosmos-db-microsoft-wants-to-build-one-database-to-rule-them-all/

Cosmos DB是微软为下一个时代准备的数据库系统。核心部件全部是用TLA+写的。

Chris Newcombe是写那篇亚马逊的论文的作者之一，他在Google groups上写了上面的一段话，表达了他用了那么多TLA+后对TLA+的看法。在他的整个职业生涯里，TLA+最有价值的是，改变了他如何工作，给了他一个很强大的工具，在系统设计层面就发现微妙的缺陷，这时系统尚未构建。一般我们编个软件出来，主要验证功能和性能，很少验证正确性。改变了他如何思考，给了他一个强大的框架，构建新的mental-model。揭示出系统设计和正确性之间精确的关系，这个关系非常重要，只有把握住这个关系，才能在后面的实现出问题时快速定位。从一个看上去好像可行的描述(例如设计文档)变成更精确的描述。在软件设计阶段就可以非常精确地把正确性定义出来。

以上是TLA+在工业界比较有代表性的反响。

从正确性来思考设计。用“科学”driven design，以前都是“猜想”driven design。

先来做几个小练习，人脑来做，加深对思路的理解。

Informal Reasoning是非形式化的推理。这个逻辑人能理解，但是计算机不能check。Formal Reasoning是计算机能check。

插入排序，每一步都将一个待排数据按其大小插入到已经排序的数据中的适当位置，直到全部插入完毕。

一个插入排序的实例：

插入排序算法如下(图中是伪码)：

插入排序Python代码如下：

def sort(nums):
    for j in range(1, len(nums)):
        curnum = nums[j]
        i = j - 1
        while i >= 0 and nums[i] > curnum:
            nums[i + 1] = nums[i]
            i = i - 1
        nums[i + 1] = curnum
    return nums

def test():
    assert [1, 2, 3, 4, 5, 6] == sort([5, 2, 4, 6, 1, 3])

    print 'test ok'

if __name__ == '__main__':
    test()

为什么算法这样写出来是对的？如果出现了Bug怎么查？要查Bug首先要知道Property。加个断点看一下A，i以前的肯定是有序的，这就是Property，无序肯定就错了。

把算法中的循环拆成一个序列 (这里i从0开始)：

S0([5 2 4 6 1 3], i=0) --> S1([2 5 4 6 1 3], i=1) --> S2([2 4 5 6 1 3], i=2) 
--> S3([2 4 5 6 1 3], i=3) --> S4([1 2 4 5 6 3], i=4) 
--> S5([1 2 3 4 5 6], i=5) --> S6([1 2 3 4 5 6], i=6)

这个属性可以描述为：对序列中的任何一个状态Si，A[0]到A[i-1]都是有序的。这是一个更加准确的描述。最终我们希望，i等于6的时候就结束了，此时A是排好序的，即：i=6蕴含着isSorted(A)，可以表达为下面的公式：

i=6 => isSorted(A)

前面讲到，对于S0到S6序列中的任何一个状态Si，都可以肯定地说A[0]到A[i-1]都是有序的，这是不变性。最终想证明上面的公式，能证明吗？

用数学归纳法可以证明。当i=0的时候，A只有一个元素A[0]，假设i=k的时候A[0]到A[k-1]是有序的，当i=k+1的时候，根据插入算法，A[k+1]前面的元素都会移动到合适的位置，A[0]到A[k]也是有序的，因此可以证明不变性蕴含了公式，通过不变性可以推导出公式。

这个不变性是一个“Inductive Invariant(归纳不变性)”。在序列的初始状态S0不变性为真，任给一个Sk，Sk+1不变性也为真，那么这个属性称为Inductive Invariant(归纳不变性)。

我们在理解一个算法时，这是非常重要的一个思想，是根本性的。通过Inductive Invariant可以推导出最终结论(属性)。程序的结果对不对，看属性是否满足就可以了。可以换种算法，例如Quick Sort(快速排序)，最终结论也是对的，但Inductive Invariant不一样。

TLA+为什么是对的，为什么能解决问题，Inductive Invariant是最核心的。

前面的描述很松散，用了很多话来描述，其实可以用公式来描述，可以用一个公式表达前面说的那么多话。

上图还是算法层面的，前面讲的层面更接近于TLA。Loop Invariant看到的还是loop，还是语言的构造，是浅层次的看法。前面讲的状态序列、Inductive Invariant是更深层次的看法，更准确。

COLUMN 4: WRITING CORRECT PROGRAMS

这本书的第4节有一个练习题，题目来自于《The Science of Programming》，一本强烈推荐的书：

这本书的作者直言不讳地说，我们的软件开发目前还处于科学前的启蒙时代，离科学还有一定的距离。这本书提出一种方法：Proof Driven Design，编程的时候一定要以“证明正确”为导向来写程序。

首先，这个过程肯定会结束，因为无论哪种方式，每次罐子里豆子的数目都会减少一个，在豆子个数有限的情况下肯定能结束。

再来看一下，罐子里最后剩下的豆子的颜色和罐子里原始的黑豆白豆的关系。白豆个数是奇数，剩下白豆；白豆个数是偶数，剩下黑豆。从数学的奇偶关系，更简洁的表达是：最终剩下白豆的奇偶性和原始白豆的奇偶性一样，即白豆的奇偶性保持不变。

思考觉得困难的时候，不要喊停，坚持下去。

为什么会有这个结果？
Inductive Invarient：每一步，白豆的奇偶性保持不变。

2b: b-1，w 0
2w: b+1, w-2
wb: b-1, w 0

b: black bean, w: white bean

以“w=3 b=2”为例，把行为序列画出来，用状态思考：

     2w       wb       2b       wb
 S0 ----> S1 ----> S2 ----> S3 ----> S4
w  b     w  b     w  b     w  b     w  b
3  2     1  3     1  2     1  1     1  0
     wb       2b       wb
    ---->    ---->    ---->
     2b
    ---->
      3        2        2        1

最下面的一排数字是状态迁移可能性总数。

如果把整幅图全部画完，涵盖了“w=3 b=2”的全部可能性，称为“w=3 b=2”取豆行为的完整图示描述。

S0到S1为什么有三种可能？
什么情况下可以取两个黑豆？b≥2。什么情况下可以取两个白豆？w≥2。什么情况下可以取一个白豆一个黑豆？w≥1 and b≥1。S0到S1的变迁有几种可能就是由这三个条件决定的。这都是很明确的数学公式，只要通过某种方法把这些显式化地表达出来，就可以通过一个公式把取豆的行为完全表达出来。取豆行为是公式的实例化。

为什么白豆的奇偶性是不变的？
再强调一下Inductive Invariant(白豆的奇偶性不变)的概念：

• 如果这个Invariant对于初始状态为真
  剩的白豆就是原始的白豆，奇偶性肯定一样。
• 且对于任何一个Si，Invariant也为真
  任何一个Si，白豆的奇偶性跟初始状态一样。

一般化一下，w=M、b=N，Inductive Invariant(白豆的奇偶性不变)：

• S0状态下，白豆的个数为M，奇偶性跟M肯定一样，Invariant为真
• 假设对于某个Si，Invariant为真，即Si状态下白豆的奇偶性和M一样，从Si到Si+1有3种可能性：2b、2w、wb，只要判断一下这3种情况下Invariant是否也为真：

2b: b-1，w 0
2w: b+1, w-2
wb: b-1, w 0

从Si到Si+1，白豆个数要么不变、要么减2，奇偶性确实没变，Invariant也为真。

通过数学归纳法证明了：白豆的奇偶性在所有状态下都保持不变。

用一种方式把行为序列描述出来，把属性用数学公式表达出来，就可以检验了，对整个行为断言，肯定知道是对的。而且只有知道了归纳不变性(Inductive Invariant)，才能真正读懂程序。

假设在任何一个状态Si下，白豆个数为Wi，用下面的数学公式可以表达这个Inductive Invariant：两个数M和Wi的奇偶性一样(两者之差一定是偶数)。

(M - Wi) % 2 == 0

【Faye】证明一下：

• 当M为奇数，可以表达为2m+1，当Wi为奇数，可以表达为2w+1，M-Wi=2(m-w)，肯定能被2整除，公式成立；
• 当M为偶数，可以表达为2m，当Wi为偶数，可以表达为2w，M-Wi=2(m-w)，肯定能被2整除，公式成立。
• 当M为奇数，可以表达为2m+1，当Wi为偶数，可以表达为2w，M-Wi=2(m-w)+1，肯定不能被2整数，公式不成立；
• 当M为偶数，可以表达为2m，当Wi为奇数，可以表达为2w+1，M-Wi=2(m-w)-1，肯定不能被2整数，公式不成立。

所以这个公式是可以表达这个Inductive Invariant的。

这是TLA+里最本质、最朴素、最核心的思想。后面的工作在于如何用一个公式来表达那么多复杂的系统。

《The Science of Programming》书里的很多方法适用于小段代码、小模块或小算法等(in the small)，在实现层面如何写出好程序。而TLA+适用于大范围、高层设计，只关心核心属性，不考虑实现。

通过这个例子对并发会有更深的理解。

http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf

这篇论文是Lamport在2009年写的。写这篇论文的初衷是一位杂志编辑邀请Lamport写一篇文章投稿到SIGACT News，因为很多并发的基础研究都是Lamport提出来的，请Lamport讲一讲如何教授Concurrency，并且建议不要写得过于细节，从高层讲讲让学习者能够Thinking Clearly，什么是Thinking Clearly，如何达到这个目标。论文写得非常好，推荐阅读。

不变性(invariance)是理解并发系统的关键，但很少有工程师或计算机科学家学到用不变量(invariant)思考。他举了一个简单的例子。

有N个进程(并发体)，编号为0~N-1，编号为0的进程称为P0，其他进程同理，它们组成一个环。每个进程有数据区x和y，初始值均为0。进程P0把X0写为1，进程P1把X1写为1，进程P1把前一个进程P0的X0读出来写入Y1，进程P0把前一个进程Pn-1的Xn-1读出来写入Y0。“x[(i - 1) mod N]”只是一种记法，表示当i=0的时候，读Xn-1，当i=1的时候，读X0。读写x或y是原子atomic操作。

这个算法满足Property：当每个进程都stop的时候，肯定有一个进程的Y等于1。类似于前面插入排序算法的属性：当i=6的时候，A肯定是排过序的。类似于Coffee Can Problem问题的属性：当取豆结束的时候，白豆的奇偶性肯定保持不变。这个属性肯定成立，因为总有一个最后的结束，总有一个进程在其他进程之后结束，最后一个进程肯定把y写为1。

【Faye】如果最后一个进程Pi写Yi时从Pi-1读取到的的Xi为0，说明Pi-1的执行落在Pi后面了，Pi就不是最后一个进程了。

但问题在于，满足这个属性并不是因为它是最后一个写Y的进程，而是因为它满足一个Inductive Invariant。

一个进程做什么只跟该进程的当前状态有关，跟那些在它之前进行写操作的进程无关。这是非常重要的一个观点。所以这个算法之所以满足这个属性，是因为它维持了一个Inductive Invariant。把过程表达成一个状态序列，找到一个Inductive Invariant，并证明Inductive Invariant蕴含/可以推导出结论Property。

重要框架
把问题(顺序、并发、Reactive、I/O)变成状态序列，选择状态，基于此找出Inductive Invariant，让Inductive Invariant蕴含正确结果，就可以保证这个结果是正确的。

Step 1：把问题变成状态序列 思考这个问题的时候，可以把N缩小。N=1时，状态序列是什么，状态序列里的每个状态有哪些状态；N=2时，状态序列是什么。

当N=1时，就是顺序程序。分别在“x[i]...”行、“y[i]...”行和“y[i]...”下一行加断点：

S0   S1   S2
X=0  X=1  X=1
Y=0  Y=0  Y=1

当N=2时，是两个进程的并发程序，会交错执行，不能加断点了，只能加日志了。假设Log是一个公共服务，Log本身不存在并发问题。日志打印进程号、X和Y的值。分别在“x[i]...”的上一行、“x[i]...”的下一行和“y[i]...”的下一行加日志，每个进程都把自己的进程号、x和y在三个地方打印出来：

log(Pi S0: x y)
x[i] := 1
log(Pi S1: x y)
y[i] := x[(i-1) mod N]
log(Pi S2: x y)

为了方便说明，作如下记号约定，日志打印出来会有几种情况？

P0A: x[0] = 1       P1A: x[1] = 1
P0B: y[0] = x[1]    P1B: y[1] = x[0]

并发其实就是组合。并发的复杂性也在于此，这么简单的程序，组合情况都不容易想清楚。而且Log不一定能打印出所有情况，因为Log打印出的序列跟当前并发平台的调度有关。

【Faye】我自己的计算过程如下：

• 注意事件顺序决定了P0A一定要在P0B前，P1A一定要在P1B前。
• 一共四个位置，第一个位置只能是P0A或P1A，对于P0A和P1A来说，剩下三个位置的组合情况是相似的。
• 以第一个位置为P0A为例，第二个位置只可能为P0B或P1A，不可能为P1B。
  • 第二个位置为P0B时，第三、第四个位置只能为P1A、P1B，1种
  • 第二个位置为P1A时，第三、第四个位置可能为P0B、P1B或P1B、P0B，2种
  • 共3种组合
• 同理，第一个位置为P1A时，也有3种组合。
• 一共是6种组合。

这个并发程序的行为就是这6种序列：

P0A P0B P1A P1B
P0A P1A P0B P1B
P0A P1A P1B P0B
P1A P1B P0A P0B
P1A P0A P1B P0B
P1A P0A P0B P1B

并发程序之所以难写，是因为在代码层面上很难看出这些序列，很难像上面那样思考问题。

如何把这6种行为序列通过一个公式描述出来呢？

• 在插入排序问题中，S0就是数组A，在取豆问题中，S0是M、N。在这个并发问题里，S0有两个，P0A和P1A，S0是一个集合(P0A, P1A)。
• 每个状态点x和y都有值。

P0A(x0=1 y0=0) P0B(x0=1 y0=0) P1A(x1=1 y1=0) P1B(x1=1 y1=1)
P0A(x0=1 y0=0) P1A(x1=1 y1=0) P0B(x0=1 y0=1) P1B(x1=1 y1=1)
P0A(x0=1 y0=0) P1A(x1=1 y1=0) P1B(x1=1 y1=1) P0B(x0=1 y0=1)
P1A(x1=1 y1=0) P1B(x1=1 y1=0) P0A(x0=1 y0=0) P0B(x0=1 y0=1)
P1A(x1=1 y1=0) P0A(x0=1 y0=0) P1B(x1=1 y1=1) P0B(x0=1 y0=1)
P1A(x1=1 y1=0) P0A(x0=1 y0=0) P0B(x0=1 y0=1) P1B(x1=1 y1=1)

在这些序列里找出Inductive Invariant，能够证明属性满足。首先要能够表达出来。TLA里的TL里很核心的一部分内容就是如何表达一个并发系统。代码里看到的并发系统是一种实现，看不到行为，更别谈属性。我们希望通过高层的描述能够把并发系统最本质的序列表达出来，而且能够清晰地定义属性，如果属性满足了就肯定是对的。

S0是一个集合(P0A, P1A)，S1也是一个集合(P0B, P1A, P1B, P0A)，为什么S0和S1有这样的关系？而且S1的四种行为都可能发生，在某种特定的调度器上可能是这种序列，换一个调度器可能是那种序列，但我们要保证不管哪种序列都是对的。这也是并发程序为何困难的原因。如果我们能够把序列的模型表达出来，能够把S0和S1之间的关系定义出来，就可以穷尽S0到S1的所有变迁，去验证并发属性，称之为“Module Check”。在测试环境下是很难复现的，因为无法穷尽所有的序列。

把序列定义出来，指明S0到S1的条件(这个条件是数学公式)，就可以涵盖所有序列，去验证属性，这称之为“Module Check”(不是证明)，再辅之以Inductive Invariant来证明，甚至可以用形式化的证明系统来证明。

后面会继续讲这道题。

并发程序和取豆程序有什么相似点？取豆程序不是并发的。P0A后面有3种可能，取豆也有最多3种可能，都是“或”的关系，感觉很像。并发是一种幻觉。所有的并发、不确定性在本质上都是一样的，本质上是一类公式，只是看如何解释，可以解释为取豆，也可以解释为并发程序。本质上一样的，都是可能满足一些条件，无论什么分支都可以走，满足一些属性。TLA就是通过这种方法完美地把顺序、并发、分布式、Reactive、I/O程序统一起来，用一种逻辑涵盖了所有系统，不管是哪一种，都是对不确定性的描述，而且可以用精确的数学公式涵盖。所谓的不确定性，无非就是或、或、或。

在上述内容中，将Debug时的状态和思考跟形式化之间建立关联，把原来手工做的事情形式化、自动化。Debug时关心的是正确性问题，Debug时肯定不关心实现语言、范式、设计模式等，关心每个点的状态变化和属性。

有一点，用Erlang和Haskell写并发程序肯定比用C/C++写可靠一些。我们讲的是本质复杂性，而不是偶然复杂性。Erlang在并发和分布式系统上肯定能减少很多偶然复杂性。但问题固有的本质复杂性，Erlang也帮你解决不了。

基于上述认识，回到一个最原始的话题————什么是一个计算？对这个问题的不同理解导出了完全不同的道路，并不是说哪个更好，只是说在一个诉求上，哪个更实用、更有效，也不会永远都好。在想实用化、有伸缩性、低层高层都能应用、不那么复杂的上下文中，哪个更容易得到正确的结论。

什么是一个计算？从这个话题展开，正式进入TLA，你会发现TLA里的东西跟前面讲的内容完全可以对应上，就非常好理解了。

或者换一个问题，如何描述一个计算？这个问题先放一放。

Computation and State Machines
http://lamport.azurewebsites.net/pubs/state-machine.pdf

这篇论文写得非常非常好，一定要看。这篇论文看完之后，再去看Paxos，理解会大不相同。这篇论文包含了一个非常重要的思想：为什么提炼出来的抽象状态，它只要是正确的，就能够证明下面的实现是正确的。这一步很重要，必须要严格证明。

在计算机科学里强调语言，这让Lamport很困扰。这种强调造成的结果是程序员是一个C++专家但他们不知道如何把程序该干什么表达出来，只是用C++表达，这只是实现，程序该干什么都淹没在程序细节里。程序应该干什么是更高层的表达。设计文档是不严格的。计算机科学领域典型的回复是：除了C++以外，程序员还需要各种正确的编程/规范/开发语言。工业界典型的回复是：程序员需要更好的调试工具。如果调试器足够好，一只猴子在键盘旁边也能自动找到代码中的错误。

Lamport认为写出更好程序的最好方法是Think better。前面讲的三个例子，就是Think better，把含糊的东西表达清楚。思考并不是玩弄语言的能力，而是玩弄概念的能力。计算机科学有很多概念，语言只是概念的一种表达，并不是概念本身。那么为什么不直接去研究概念而是研究语言呢？要想得更清楚，要思考概念等更基本、更本质的东西。语言会塑造思考，语言是双刃剑，一方面语言好一点思考得好一点，另一方面语言也会限制思考境界，跨过语言边界，很多东西就忽视掉了【Faye：实在听不清？】。那么如何能够不被语言干扰？Lamport的回答是：像其他科学工程分支一样，用数学来表达，不要再发明语言来表达。现实中是否有可操作性呢？后面回答了这个问题。

Lamport举了物理学家关于E=mc2的例子，反映了计算机科学的现实。Computation是计算机科学里一个非常重要的主题，每一个可以计算的实体都可以表达为一个状态机。计算机科学家太过于关注语言，大部分都没有觉察到那些语言都是在描述状态机。

如果是在正确性这个上下文里，我们在Debug的时候关心的就是一步一步的状态，不关心语言是什么样的。如果在正确性里非要把语言加进来，会造成障碍。Lamport关心的上下文是正确性，他认为正确性和代码的清晰组织是正交的，代码组织得很好并不代表它正确。我们在设计层面上强调模块化，分而治之，但在正确性方面，Lamport认为这是错误的，不可能小模块正确、核心函数一定正确【Faye：实在听不清？】，特别是在并发系统。一个面向对象设计很好的系统一旦面对并发就土崩瓦解，一旦加锁各种问题都出来了。还不如直接用状态机描述序列，直接去看它的性质，就可以知道是否正确。为何非要搞一个语言，语言里看不到堆栈、pc，想去解决问题的话可能会很复杂，只能通过外面的东西观察是否存在，而不能截取看是否存在，这就很复杂了。Lamport认为搞这么复杂完全没意义，状态机就够了。

状态机为大部分计算机科学提供了一个框架。它能用非常普通的、简单的数学来描述，例如集合、函数和简单的逻辑。通过状态机可以把“计算”这个概念用非常简单的数学统一描述，不管是哪个领域，编译、分布式、并发等。如果过于偏重语言，在想去统一计算机科学不同领域时会造成很大的障碍。举个例子，大家都学过Functional Programming语言，例如Erlang、Haskell，程序如果是顺序的，没有副作用、没有时间、函数可以任意组合跟数学公式一样，但一旦涉及到I/O、并发，大家学过Monad，很难理解，为什么？用Functional Programming，对顺序的、纯的特性用一种方式，对Side-effect的特性还得用另一种方式，如果想统一的话，得找一个更复杂的方法把它们统一起来，Monad就是干这个事情的，把I/O、State、Concurrency、顺序程序统一起来，很复杂很难理解。但Monad对于程序的功能化是有意义的，对正确性是没有意义的。想保证实现层面的组织化和清晰化，Monad还是有作用的。

如果一个人基于语言层面思考，语言层面的不同就会把一些很根本的相似性模糊掉，找不到相似性，因为关注语言去了。这也是Lamport写一篇论文40年后还有用的原因，就是因为不关注语言，只关注基础相似性。

如果用语言表达的话，一个简单的概念会变得很复杂。如果语言不能表达一个概念，这个必要的概念就不能被引进。例如，汇编语言可以表达堆栈，高级语言没法表达堆栈，堆栈的概念就看不见了。在技术里也有“政治正确”的概念，其实就是不同的术语，例如完全抽象(full abstract)、可观测的(observable)和指示的(denotational)等，说起来很高大上，政治正确但不解决实际问题，或者说，就目前来说，解决实际问题的效果不是那么好。

我们做的所有事情都是在描述Computation。下面这些都是对计算的描述，有具体的硬件、抽象的机器、具体的语言描述：

• 自动机，包括图灵机、摩尔机、...、细胞自动机等
• 用编程语言写的计算机程序
• 用自然语言或伪码写的算法
• 冯·诺依曼计算机
• BNF语法
• Robert Floyd和Tony Hoare写的进程代数，也是一种逻辑

Lamport认为这些都可以描述成状态机，这样就统一了，特别是关注正确性的话，状态机就够了，而且实践效果非常好。举个例子，BNF用于描述语言的语法，起始符、终结符、非终结符、产生式/规则，从语法导出程序，如何用状态机描述？状态机的S0就是所有的起始非终结符，从Si导出Si+1就是把里面的所有非终结符通过产生式替换成下一个非终结符或终结符。

沃尔夫综合症：混淆了语言和现实。本来是解决实际问题的，发明了语言，关注语言不管现实。现实明明有堆栈，语言不允许有堆栈。导致的结果就是，这些设备用不同的语言描述，它们肯定是不一样的，但其实它们都是一样的，可以用状态机描述。同理，从语言层面思考，并发系统和顺序系统不一样，但从状态机思考，它们没区别。

一个是实物、一个是对实物的符号描述，经常混淆。例如，higher-order是一个非常政治正确的词，higher-order只是一种对系统的描述，系统本身不一定有higher-order。解决问题的时候，思考用什么工具，问题本身反倒被抛开了。即使用数学也可能会出现这个症状，只是降低了很多可能性，更关注数学本身而没有关注现实。要向物理学家学习，物理学家在研究问题的时候能够非常清楚地区分现实和解决现实的形式化部分。

想用一个带procedure的程序语言来表达状态机，在状态机里没法表达call stack。用C语言写状态机，没法写call stack。但call stack中的数据变化对正确性来说至关重要，只能加断点调试。沃尔夫综合症引入一些限制，为把程序表达成状态机增加了困难，导致在你想去推理一个程序的时候会带来很多不完备性。

我们写过很多状态机，但那都是实现。这里是状态机的数学定义。

一个状态机包括一个状态的集合(S)，一个初始状态的集合(I)，从Si到Si+1如果满足一个关系R(N)，那么I是S的子集，且R是S×S(笛卡尔积)的子集。然后会产生所有的计算S1->S2->S3->...序列。满足以下两个条件： S1属于I，(Si, Si+1)属于R。

还是来看取豆的例子。

我们一直认为初始状态就是“b=M、w=N”，这里的等号不是赋值，而是数学公式里的等号。我们设计一个系统，系统原本是不存在的，现在建立一个系统，有很多行为，这样理解是错误的。应该认为所有的行为、所有的状态在整个宇宙里都已经存在了，要设计的所有系统全部都已经存在了，目前设计的系统只是说要写出一个条件把期望的状态和行为序列过滤出来。这是一个非常重要的想法。“b=M、w=N”的意思是：在现实宇宙中有很多b、w，b和w什么值都有可能，定义b=M、w=N，最终产生一个布尔值，希望从宇宙空间里把b等于M且w等于N的S作为S0。正是基于这样的设计，我们才能把不同层次的实现通过逻辑关系构建起来，非常优雅地去做各种规范的组合。可能有很多状态量，但只关心x、y，因为其它状态量跟目前的属性无关，S0包含了所有属性，各种值都有可能，现在只关心跟属性相关的值。“b=M、w=N”是过滤条件。同理，在宇宙里从这个状态到那个状态，每个状态都有关联，所有行为都有，从任何一个Si都可以到任何一个Si+1。取豆的时候取任何个数都有可能，取3个也是有可能的，现在希望取2个。我们写的布尔逻辑也是过滤，通过这个布尔逻辑把那些取3个的、以及取2个之后没有放回去或者放回去不合适的全部过滤掉，只留下我们希望的行为。

在取豆的例子中，R就是if b>2 ... 、if b<2 ... ，就是Relation(过滤条件)。

S和I都是Universe，S1是一堆Filter的结果，Si和Si+1属于R，R是我定义的，因为宇宙里有很多Si到Si+1的关系，选择满足R的关系。我们写的初始S1、Si到Si+1的关系，都是布尔表达式，目的在于从整个宇宙行为中把我们定义的行为过滤出来。而不是说行为不存在，我们定义出新的行为。

假设状态x和y，在语言中写x=0、没有写y，y的值不变，但在TLA里写x=0、没有写y，则表明y可以是任意值，TLA通过这种方式来完美容纳不确定性。

宇宙蕴含了一切可能，我们找出我们需要的行为。

• ODE - Dynamic Continuous System
• TLA+ - Dynamic Discrete System

做一个类比。

物理学家在研究地球围着太阳转的时候，是一个动态连续系统，他们用常微分方程描述动态连续系统。状态的表达跟当前关心的行为有关，我们关心当前的位置(三维坐标)、速度、方向，这就是当前状态，在t时刻是这样，在t+△t时刻的行为可以通过一个方程式来表达。地球围绕太阳转的轨道、炮弹打出去的轨道都可以通过常微分方程描述。一个方程式蕴含了系统的所有行为，通过方程式可以判断正确性问题。

TLA+等同于解决动态离散系统的常微分方程。状态通过公式描述出来，行为全涵盖了，可以assert属性。

直接用普通数学来表达状态机。用变量和它们的范围来表示状态的集合。例如地球围着太阳转，我们关心位置坐标、初始速度、方向。状态跟诉求有关，解决不同的问题，状态可能不一样。然后，每一时刻值都会变化，这里的变化是一种关系，在时刻t和t1之间的关系，这个关系表达为方程。

在取豆问题中，假设在S0状态下w=5、在S1状态下w=3，都是w在不同时刻的值，如何表达？加'(prime)。假设X是Si的值，那么X在Si+1的值是X'。

X' = X + 1

这不是赋值，这是Relation。

Init(S0): X = 0
Relation: X' = X + 1

序列“0 1 2 3 4”满足上述公式，而序列“0 1 4 ...”不满足上述公式。

The benefits of describing state machines mathematically rather than hiding 
them behind computer-science languages would make a long list. It might begin 
with the replacement of esoteric programming logics by ordinary mathematics.

... two alogrithms that appear unrelated until they are expressed 
mathematically as state machines.

... The obsession with language is a strong obstacle to any attempt at 
unifying different parts of computer science. When one thinks only in terms of 
language, linguistic differences obscure fundamental similarities.

【Faye】PPT照片拍糊了，人工输入了一下。

这个例子取材于《Computation and State Machines》论文。

fact1(int n) {
    int f = 1;
    for(int i = 2; i <= n; i++)
        f = i * f;
    return f;
}

fact2(int n) {
    int f = 1;
    for(int i = n; i > 1; i--)
        f = i * f;
    return f;
}

fact3(int n) {
    return (n <= 1) ? 1 : n * fact3(n - 1);
}

这三个程序都是用来算阶乘(factorial)的，哪两个相似性更高？
从状态机的角度思考，fact1和fact3比较像，都是从1开始计算，拥有相同的乘法序列，而fact2则不然。或者这样想，把乘法改成减法，fact1和fact3的结果是一样的。注意乘法满足交换律，减法是不满足交换律的。

【Faye】老师PPT中的程序和论文中的不一样，区别在于fact1和fact2中for循环中的语句。论文中的是“f = i * f”，PPT中的是“f = f * i”，乘法没区别，减法就有区别了。如果按PPT中的程序，fact1和fact2的结果是一样的。如果按论文中的程序，fact1和fact3的结果是一样的。

如果用PPT中的“f = f * i”，乘法换成减法后是“f = f - i”，假设n=7，计算过程如下：

fact1:
1 - 2 = -1
-1 - 3 = -4
-4 - 4 = -8
-8 - 5 = -13
-13 - 6 = - 19
-19 - 7 = -26

fact2:
1 - 7 = -6
-6 - 6 = -12
-12 - 5 = -17
-17 - 4 = -21
-21 - 3 = -24
-24 - 2 = -26

fact3:
(7 - (6 - (5 - (4 - (3 - (2 - 1)))))) = 4

Python程序运行结果：

>>> def fact1(n):
    f = 1
    for i in range(2, n + 1):
        f = f - i
    return f

>>> def fact2(n):
    f = 1
    for i in range(n, 1, -1):
        f = f - i
    return f

>>> def fact3(n):
    return 1 if n <= 1 else n - fact3(n - 1)

>>> fact1(7)
-26
>>> fact2(7)
-26
>>> fact3(7)
4

如果用论文中的“f = i * f”，乘法换成减法后是“f = i - f”，假设n=7，计算过程如下：

fact1:
2 - 1 = 1
3 - 1 = 2
4 - 2 = 2
5 - 2 = 3
6 - 3 = 3
7 - 3 = 4

fact2:
7 - 1 = 6
6 - 6 = 0
5 - 0 = 5
4 - 5 = -1
3 - (-1) = 4
2 - 4 = -2

fact3:
(7 - (6 - (5 - (4 - (3 - (2 - 1)))))) = 4

Python程序运行结果：

>>> def fact1(n):
    f = 1
    for i in range(2, n + 1):
        f = i - f
    return f

>>> def fact2(n):
    f = 1
    for i in range(n, 1, -1):
        f = i - f
    return f

>>> def fact3(n):
    return 1 if n <= 1 else n - fact3(n - 1)

>>> fact1(7)
4
>>> fact2(7)
-2
>>> fact3(7)
4
>>> 

从语言结构上，fact1和fact2很像，都是迭代循环，fact3是递归，人工比较一下才会意识到fact1和fact3很像。如果把程序用状态机表达，一眼就能看出来。编程语言的语言构造掩盖了计算本质。

fact3把递归改成非递归，加一个堆栈，变复杂了，压栈出栈，TLA也可以表达这种堆栈，即使这样写，还可以从数学上证明fact3堆栈的写法跟fact1是一样的。

用TLA描述一个状态机，层次是可以选择的，可以选择非常高的层次，也可以选择非常低的层次。对于同一个算法，由于选择的层次不同，描述会有所不同。用A1表达一个算法，用A2表达另一个算法，A2只是比A1多了一些细节，如何能保证A1里证明的属性A2里都满足呢？这是一个非常重要的特性，如果没有这个特性，一切都是白搭。

下面举个简单的例子，通过这个例子了解什么是真正的抽象(Abstraction)。

第一个算法很简单，可以认为是一个编程语言。程序X，循环交替执行P和C。如果打印Log的话，序列为：P, C, P, C, ...。用Init(初始状态)和Next(Relation)把这个序列表达出来。

loop/endloop的本质是goto，对产生这个序列至关重要的状态是pc指针。在P上加一个Label 0，在C上加一个Label 1，当pc=0时执行P，当pc=1时执行C。

引入pc，把程序改为：

loop
    0: P
    1: C
endloop

pc=0 P
pc=1 C 

序列：P C P C P C ...
      0 1 0 1 0 1 ... (pc)

pc是控制状态，程序里看不见，但是要把它表达出来。

写Init，写一个Filter，把所有需要的过滤出来；写Next，写一个Relation，把满足Relation的序列过滤出来。

Init: pc = 0
Next: if pc = 0
        pc' = 1
      if pc = 1
        pc' = 0

以上都是逻辑公式，对它们求值的话都是布尔值。就是说，任给两个状态Si和Si+1，让pc=Si，pc'=Si+1看公式是否为True。序列0 1 0 1 0 1 ...是满足的，如果把if pc = 1分支的pc' = 0改为pc' = 2，序列0 1 0 1 0 1 ...就不满足了。要么公式写错了，要么算法写错了。

程序加上pc控制状态就可以描述程序的行为。程序看起来好像更简单，pc表达好像更复杂，但其实简单没用，因为它漏掉了重要的东西，把pc隐藏起来看不见了。

第二个算法是两阶段握手协议，硬件里用得比较多，Prod可以认为是发送者，Cons可以认为是接收者，可以认为是两个收发进程。Prod和Cons之间有两个电平线p和c。两个电平线会被置位，发送进程Prod会给p置位，接收进程会给c置位。如果p和c的电平一样，就发送，然后把p改变一下，改成跟c不一样，然后C检测到p和c的电平不一样，就接收，然后把c改变一下，改成跟p一样，然后P检测到p和c的电平一样，又发送，然后把p改成跟c不一样……。这是一个并发系统。

程序Y，P可以认为是发送数据，C可以认为是接收数据。圆圈中间一个加号的符号是“异或”。

理解一个系统最好的方法是，举个简单例子把序列写出来。刚开始p=c=0，序列为：

p=0   P   p=1   C   p=1   P   p=0
    ---->     ---->     ---->     ----> ...
c=0       c=0       c=1       c=1

希望系统有“P和C交替执行”的性质，这样才符合两阶段握手协议的规范。那么这个设计是否能够满足规范要求呢？

再看第一个程序X，很简单，一看就知道P、C交替执行。当然程序Y也没那么复杂，但如果不多想一下，一下子不一定看得出来。如果能够证明Y是X的一个实现，就是说，如果某个性质在X上是满足的，在Y上一定是满足的，我们称“X是Y的抽象，Y是X的实现”。我们可以用数学公式表达X，也可以用数学公式表达Y，这样就把Y的正确性问题变成X的正确性问题。X比较简单，一眼就能看出来，就可以证明X是正确的，然后Y也是正确的。

现在的问题在于，如何能够证明Y的所有行为都是X的行为。我们写了一个公式，这个公式是状态序列，每一个状态序列是一种可能行为，就像取豆一样，有很多种可能性，这个公式表达了所有行为。如果Y的所有行为都是X的行为的话，那么对于X的所有行为上都满足的属性，Y一定满足。Y有3种行为b1、b2、b3，X有5种行为b1、b2、b3、b4、b5，证明了属性P对于X里的每一个行为全部都满足，b1、b2、b3肯定满足，Y肯定满足。Y的所有行为集合是X的行为集合的子集，X满足的属性，Y肯定满足。

下面来看看，能否证明从X导出Y，或者Y的所有行为集合是X的行为集合的子集，那么X满足的属性，Y肯定满足。这是一种非常常用和最核心的方法，在TLA里称为refinement(精细化)。越精细化，越偏重实现，确定性越少。行为越多，确定性越少。层次越高，包含的确定性越多，但并不希望属性减少。实现层面上的状态非常多，在这个层面上证明正确性是非常困难的，如果能够把状态逐渐减少，变成一个相对简单的描述，也就是抽象，但关心的属性并未丢失，就可以在相对简单的层面上证明属性，然后由于实现的行为是抽象的行为的子集，抽象满足的属性，实现肯定满足。

Y复杂，X简单。类比一下，把Y看成平时写的程序，如果只想看P、C是否交替执行这个属性，很多细节就不用看了，只需要关心，如果X和Y之间有关系的话，X正确，Y肯定正确。

上图中，Initx中的Initpc先不用管，只需要看pc=0即可。if/else其实是一个“或”的关系，“\/”表示“或”，“/\”表示“与”，都是布尔表达式。在一个行为或状态序列(行为就是状态序列)里，Si状态下的“pc=0”条件为真，P没什么关系先不关心，下一个pc(pc')=1为真的话，Nextx就为真了；要么pc=1、pc'=0，Nextx也为真。这样就描述了一个状态序列。这是描述了一种，如何描述多种，后面会讲。核心在于如何通过一个公式描述一种或多种不确定的状态行为。这是TLA最核心的思想。

上图中，Inity中的Initpc先不用管，只需要看p=c即可。Nexty是Prod和Cons布尔或。Prod中为何要写“c'=c”？不能不写，如果不写的话，表示不确定，c'可以为任何值，而这里是要表示c不变的意思，这是过滤条件，一定要精确。

现在来看Y的公式为真是否蕴含了X的公式为真，即要证明Y => X (Y Imply X)，Y的所有行为都是X的行为。

在X的公式里是pc一个变量，在Y的公式里是p和c两个变量，要证明两个公式之间有什么关系的话，必须建立一种关系。

X    Initx = pc=0

Xbar Initxbar p c

Y    Inity = p=c

在X和Y中间找一个中间步骤Xbar(记法是X上面有一横)，也有变量p和c，Xbar跟X有关系、跟Y也有关系，进而导出X和Y之间的关系。举个例子，A和C不知道谁个子高，中间有个B，如果A比B高、B比C高，那A肯定比C高。

在数学上，一个函数可以任意替换一个变量。假设有一个函数φ，接收两个变量p和c，具体是什么暂时不知道，需要定义出来，令pcbar(记法是pc上面有一横)等于φ(p, c)：

X    Initx = pc=0

Xbar Initxbar p c  pcbar = φ(p, c) = ?

Y    Inity = p=c

由于Initx = pc=0，可以让φ(p, c)=0。由于Inity = p=c，要在φ(p, c)=0和p=c之间建立一个恒等于(记法是=上有一横)的关系，即φ(p, c)=0当且仅当p=c。这是我们对φ函数的要求。那么φ函数是什么呢？

X    Initx    = pc=0
       |
Xbar Initxbar = φ(p, c)=0  pcbar = φ(p, c) = if p=c 0
       |         |||                            p≠c 1
Y    Inity    = p=c

Nextx里有pc=0和pc=1，同理，把pc=1替换成φ，跟Nexty之间建立恒等关系。

通过引入φ函数建立一个映射关系，对于Initx的所有状态序列，里面关于pc的论断在Xbar里全都正确。把pc映射成pcbar，把Initx = pc=0中的pc写成pcbar也没错，把φ(p, c)映射成pcbar=0，其实就是p xor c (xor的记法是圆圈中间一个加号)。

就是说，对于φ(p, c)中的任何p和c，都通过这个映射变成pc。Initx的状态序列S1->S2->S3->...，Initxbar的状态序列S1bar->S2bar->S3bar->...。再定义一个φ，接收一个序列，它把序列S1->S2->S3->...变成序列φ(S1)->φ(S2)->φ(S3)->...。

φ(S1, S2, S3, ...) = φ(S1), φ(S2), φ(S3), ...

通过φ函数把p和c变成一个变量pcbar。在φ变换下，序列S1->S2->S3->...和序列φ(S1)->φ(S2)->φ(S3)->...是同构的，由于P和C是没有任何设计的，这样就可以保证Initx的S序列中的任何属性的论断在Initxbar中都满足。这是一个成功的映射。

上图中，右边的pcbar就是φ函数，把p和c映射成pc(记为pcbar)，P和C保持不变：

• pcbar等于0当且仅当p=c：
  • 替换左上角Initx中的pc=0，就是左下角Initxbar中的p=c。
  • 替换左上角Nextx中的pc=0和pc'=0，就是Nextxbar中Pr和Co中的p=c和p'=c'。
• pcbar等于1当且仅当p≠c：
  • 替换左上角Nextx中的pc=1和pc'=1，就是Nextxbar中Pr和Co中的p≠c和p'≠c'。

可以看到Initx、Nextx和Initxbar、Nextxbar是完全等价的。由于P和C没有任何设计，所以P和C在两个序列里性质保持不变，只是pc和p、c之间有关系。

那么，Initxbar、Nextxbar和Inity、Nexty有什么关系呢？

Initxbar、Nextxbar和Inity、Nexty都有p和c。Nextxbar中Pr的p'≠c'什么时候成立？要么是p'=p xor 1，要么是c'=c xor 1。如果Nexty中的Prod和Cons为真，那么Nextxbar中的Pr和Co一定为真。Nextxbar包含更多的行为，因为Nextxbar的Pr可以包含p不变和c不变，而Nexty的Prod只包含了c不变，所以Nextxbar的序列更多、Nexty的序列更少。只要是Nexty的行为，一定是Nextxbar的行为。如果Nexty为真，Nextxbar一定为真，即 Nexty => Nextxbar。而Nextxbar又等同于Nextx，所以Nexty => Nextx。对于p和c来说，如果Nexty为真，Nextx一定为真。也就是说，Nexty的所有行为都是Nextx的行为。反过来说，如果Nextx的所有行为都满足某个属性，Nexty的所有行为一定满足，因为Nexty的行为是Nextx的行为的子集。

TLA的核心在于，可以通过抽象、建模把一个很复杂的实现基于想关心的属性把它提炼出来，因为抽象层面简单、好证明，实现层面复杂、不好证明，而且可以证明两者之间有Imply关系，就可以了。通过TLA写Spec，可能只有200行，可以证明数十万、上百万行的程序实现的设计思想是正确的，实现本身的错误是另外的问题。复杂的事情可以通过抽象变成简单的事情，而且抽象的过程要保证属性不变。

附上老师PPT中的一些文字截图，供参考理解：

上述内容在《Computation and State Machines》论文里有提及但并不详细，详细的内容在下面这篇论文里：
The Existence of Refinement Mappings http://lamport.azurewebsites.net/pubs/abadi-existence.pdf

用多种数学法都可以表达这个问题，但用编程语言没法表达，根本没法做替换，没法做映射，没法表达逻辑关系，编程语言里没有蕴含关系。

TLA里严格定义了抽象(Abstraction)和实现(Implementation)，实现也叫精细化(Refinement)。

X => Y是一个命题，X实现了Y，或Y抽象了X。公式X表达的所有行为/状态序列[X]是公式Y表达的行为/状态序列[Y]的子集。这样在Y做证明，就可以证明X。后面的核心问题在于，如何通过公式来表达各种各样现实中的程序，例如并发程序、分布式程序、I/O等。

Time, Clocks and the Ordering of Events in a Distributed System
http://lamport.azurewebsites.net/pubs/time-clocks.pdf

The Part-Time Parliament
http://lamport.azurewebsites.net/pubs/lamport-paxos.pdf

这是Lamport的两篇经典著名论文。

Paxos算法很复杂，但用TLA+写只有不到100行程序。

状态机、关系、实现与替换。

• http://lamport.azurewebsites.net/pubs/pubs.html, Leslie, Lamport
• The Science of Programming, David Gries
• Specifying Systems, Leslie Lamport

本课程的内容是关于软件设计“正确性”的。在日常软件开发过程中，我们通常会采用编写设计文档、设计评审、代码走查、简单设计、分层测试等方法来保证软件设计的正确性。这些方法都是必要的，但对于固有复杂性很高的软件系统，例如并发、分布式系统等，是远远不够的，系统设计中的微妙错误很难通过这些方法发现。

那么，如何做“正确性”设计，或者说，如何用科学的方法表达出希望系统做什么。用软件系统设计文档表达无法做到精确，这才有了“源代码就是设计”，用代码表达确实精确，但由于编程语言的关系，混杂了很多实现层面的细节，无法清晰地呈现设计，难以保证正确性。

那么，用什么来表达呢？TLA+，由2013年图灵奖得主Leslie Lamport发明。Lamport是一位应用数学家，他的研究领域是计算机科学。他非常务实，而且能够长时间地清晰思考。

早在1949年，Alan Turing就写过一篇论文《Checking a Large Routine》，讲述了如何从正确性检查例程，这篇论文虽然并未广泛流行，但思想很深远。Robert Floyd和Tony Hoare受这篇论文影响，在此基础上发明了Floyed Hoare Logic，属于语言派。Lamport刚开始是跟随Robert Floyd和Tony Hoare，后来与他们产生了分歧，发明了TLA+，属于计算派。语言派是站在语言层面的视角，语言能描述的东西才能存在、才能看到，语言不能描述的东西就不存在，例如程序的Control State、Call Stack、pc指针等；但计算派站在计算层面的视角，关注计算层面的概念，只要概念存在就可以拿过来用，让Control State、Call Stack、pc指针等显式化，就可以把并发程序、分布式程序、批处理程序、I/O 、Reactive等全部统一在一个简单框架里。

TLA+的全称是Temporal Logic Action Plus。TL是Temporal Logic(时态逻辑)，是由Amir Pnueli在1977年发明的。但Temporal Logic过于复杂、很难理解，Lamport为了让一线程序员能够使用，对Temporal Logic做了大量简化，发明了TLA。TLA用来描述动态的系统行为，但不包含静态状态。于是Lamport又发明了TLA+，他选择用数学的集合论和一阶逻辑来描述静态状态。

TLA是一个逻辑框架，为了便于从直觉上理解它，可以深入思考一下我们再熟悉不过的Debug。形式化以后的Debug如下图所示：

当系统运行出问题的时候，换句话说，当系统未按照我们的期望运行的时候，我们开始加断点调试。我们对系统行为的期望，即Property。这些期望跟实例化无关，无论用哪种编程语言或者编程范式。每个断点断下来以后，都对应一个系统的状态，例如S1、S2、S3、……。在Program/Implementation层面会有很多状态变量，但我们不会查看所有状态变量，而是基于对业务的理解，查看其中的某些状态变量，这些状态变量可能是程序里有的，也可能是程序里没有的，例如Call Stack，这些都是在我们大脑中的，是Abstract的。系统运行起来以后，Program中的值不满足Brain中的判断，就可以定位出系统哪里出了问题，这就是我们平时的Debug。

Implementation蕴含了Abstract，如果Property中关于状态变量的论断在Abstract中是正确的，那么在Implmentation中就一定是正确的。如果Abstract违反了Property，Implementation一定也违反了Property。

TLA+可以用来描述这些状态、迁移和属性，并且能够保证Implementation蕴含Abstract。

TLA+是一个逻辑框架，有很多优点：

• 可以统一描述顺序、并发、分布式、Reactive、I/O等各类系统；
• 既可以描述Abstract层面，也可以描述Property;
• 只关心核心属性，不考虑实现；
• 从高层设计到低层设计都可以使用TLA+；
• 伸缩性好。(【Faye】还不是很理解这里的伸缩性是什么意思)；
• 基于数学，本身简单。

TLA+的语法和语义都很简单，但绝不是玩具，它非常强大，在Amazon Web Services、欧洲航天局的RTOS、微软的Cosmos DB都有成功的应用。

Lamport认为写出更好程序的最好方法是Think better(【Faye】我理解就是清晰地思考)，要清晰地思考概念等更本质的东西，不要受到语言的限制。那么，怎么才能不被语言干扰呢？Lamport给出的答案是：像其他科学工程分支一样，用数学来表达。、

通过Insertion Sort、Coffee Can Problem和Teaching Concurrency这三个例子，我能深深体会到平时的思考是多么的肤浅和模糊，远远达不到接近本质和清晰。在这个三个例子中，有几个关键点要反复思考和仔细体会，反正我自己以前从来没有以这样的方式去思考过问题：

• 系统的属性是什么。
• 如何用公式表达系统的属性。
• 选择状态，把系统行为的状态序列描述出来，找到Inductive Invariant(归纳不变性)，即对于序列的所有状态不变性均为真。用数学归纳法证明，Invariant对于初始状态S0为真，任给一个Sk，对于Sk+1不变性也为真，就可以证明Invariant对于序列的所有状态均为真，即Inductive Invariant。
• 用数学归纳法可以证明Inductive Invariant蕴含了属性，即通过Inductive Invariant可以推导出属性公式。
• 如何用公式表达Inductive Invariant。
• 从这样的角度思考，并发程序和顺序程序并没有本质区别，其他不同类型的系统也同样可以被统一在这个框架里。
• TLA+之所以能解决问题，找到Inductive Invariant是最核心的。
• 定义序列，指明从S0到S1的条件，就可以涵盖所有序列，从而验证属性，即为Module Check。
• 思考觉得困难的时候，不要喊停，坚持下去。

基于上述认识，重新思考一个非常原始的问题————什么是一个计算？
Lamport认为通过状态机可以把“计算”这个概念用非常简单的数学统一描述。使用语言来描述，容易患上沃尔夫综合症，将语言层面导致的差异误认为是本质的差异，把问题搞复杂了。

用状态机思考问题的时候，要时刻提醒自己：所有的行为和状态在整个宇宙里都已经存在了，目前设计的系统只是要写出条件把定义的行为状态序列过滤出来。用以下步骤描述状态机：

1. Init：写Initial Predicate过滤出所有初始状态。
2. Next：写Next-state Relation过滤出所有的状态序列。

Factorial的例子形象地告诉我们，编程语言的语言构造是如何掩盖了计算本质。同样实现了P/C交替执行的两个程序的例子展示了TLA+里一个非常常用和最核心的方法refinement(精细化)。实现层面上的状态非常多，很难在这个层面上证明正确性(满足属性)，如果能够提炼状态并保证关心的属性不丢失，即做一个抽象，就可以在相对简单的抽象层面上证明正确性，然后由于实现蕴含了抽象，实现的行为是抽象的行为的子集，抽象满足的属性，实现肯定满足，从而证明了实现的正确性。

接下来的核心问题在于，如何用公式表达各种各样现实中的程序。

最后，我还有一点感想，跟TDD、DDD/DSL一样，TLA+也只是工具，清晰地思考是最重要的，也是无法替代的核心竞争力。