前言
"If you don't know where you're going, it doesn't really matter which path you take."
—(Lewis Carroll, 1832–1898)
"You got to be careful if you don't know where you're going, because you might not get there."
—(Yogi Berra, 1925–)
"The worst thing about new books is that they keep us from reading the old ones.''
—(Joseph Joubert, 1754–1824)
如果一个系统满足他的设计需求，那么这个系统是正确的。这点非常被认可。但是如果我们设计的系统是软件的一部分，特别是如果它涉及到并发，那我们如何展示这一点？仅仅展示这个系统可以满足它的需求是不够的。一些测试通常足以证明这一点。真正的测试是表明系统不能满足其要求。
Dijkstra关于测试[1] 的众所周知的格言尤其适用于并发软件：并发系统执行的非确定性使得很难设计出具有足够覆盖范围的传统测试套件。这里存在一些基本问题，涉及分布式系统执行中事件的可控性有限以及这些事件的可观察性有限。[2]
[1] The quote "Program testing can be used to show the presence of bugs, but never to show their absence" first appeared in Dijkstra [1972], p. 6. The quote has a curious pendant in Dijkstra [1965] that is rarely mentioned: "One can never guarantee that a proof is correct, the best one can say is: "I have not discovered any mistakes.""
[2] For instance, process scheduling decisions made simultaneously by different processors at distinct locations in a larger network.
精心设计的系统可以满足其设计要求。但是，如果我们用标准测试方法无法达到这种程度的确定性，那我们还能做什么呢？使用标准数学在这个领域并不是一个很好的选择。即使是简单的分布式程序的全面手工证明也可以挑战最强硬的数学家。乍一看，机械验证程序似乎也没有多大希望：很久以前就已经证明，根本不可能为任意程序构建一般证明程序。[3] 所以给出了什么？
[3] The unsolvability of the halting problem, for instance, was already proven in Turing [1936].
幸运的是，如果满足一些适度的条件，我们可以机械地验证分布式系统软件的正确性。本书的主题是展示这些“适度条件”是什么以及我们如何使用相对简单的基于工具的验证技术来解决苛刻的软件设计问题。
