概述
- 并发系统的正确性是很难证明的，因为异步点太多，人类的大脑不是为并发而进化的，并发系统的行为变化可能性太多
- 如果能够把系统的状态/行为抽象为时态逻辑（Temporal Logic），结借助CPU超强的算力，穷举出所有可能的behavior（状态序列）就可以判断系统是否正确
- 基本的TLA+语法和使用可见状态序列是指数级别，需要深入立即系统和TLA+对状态进行剪枝
- 什么是Temporal Logic：系统随着时间的推移，可能出现的状态序列
- TLA+是基于数理逻辑的语言，如果你对数理逻辑很有研究，那么会如鱼得水
What is a specification?
- spec描述应该实现什么，而不是描述如何实现
- 用来验证设计，而不是教你如何设计
- 在动手coding之前，进行specify能帮助你更好的理解你的系统
- 只验证设计是否正确而不验证性能
- specification的基础是数学，因为只有数学语言是精确的
- 这里用到的数学是更加形式化的数学，而不是我们在学校时学到的经典数学（大部分也不是精确的）。形式化的数学看起来很冗长，但是能用最少的数学概念描述一个系统。
Why TLA+
- 1977年，艾米尔.伯努利用时序逻辑temporal logic来specify一个系统，但是只能描述部分系统
- 1980年代，Lamport发明了TLA（temporal logical action），选择了数学家们（而不是程序员）所喜爱的一阶逻辑理论和集合理论
- TLA提供了specify系统的数学基础，数学描述现实的系统，TLA来形式化数学：TLA就是来解决如何用程序描述数学的问题，而TLA+就是这门语言，仅仅借鉴了编程语言的模块化的思想，除此之外都是数学概念
- TLA+可以方便描述任何离散的系统（因为它建立于集合论），尤其是异步系统
- TLA+使用简洁的数学语言来描述状态转换
- TLA+不是用来描述程序执行的指令序列
一个例子
- C语言代码
int i; void main() { i = someNumber(); i = I + 1; }
- 和这段代码等价的spec是下面这段tla（emacs上可以安装一个插件，以prity-print方式显示希腊字符）
- 几点说明：
- TLA+支持以模块方式组织代码
- 以——————————— MODULE SimpleProgram ----------------------开始
- 以====================================================结尾
- 任何TLA+ spce都要有Init和Next，Init和Next被称为formula
- TLA+会默认用Init进行初始化状态，默认用Next迭代可能到达的状态
- Init == (pc = "start") /\ (i = 0), ‘==’ 定义一个 formula
- 逻辑与运算符‘/\’：a /\ b 表示先发生a，再发生b
- 逻辑或运算符‘/’：a / b 表示要么发生a，要么发生b
- Next formula描述的是一个状态机，‘/’运算连接起来的是两个状态入口“start”和“middle”
- pc’ 和 i’ 是下一个状态中pc和I的值，记做(pc primae, i prime)
- TLA+ 使用宽度遍历，暴力遍历所有可达的状态
总结
- 任何系统都能够使用状态机描述
- specify状态机所有可达的状态
- TLA+使用CPU超强的算力穷举所有可能的状态序列
