CHAPTER 1 Why Prove the Correctness of Program

传统工程学有标准的数学工具来设计工业产品。能保证产出的安全性和适用性。这些标准或多或少，在工程师设计阶段会被考虑到。由于标准从更高角度严格制定，所以根据标准进行的设计安全性是有保证的。

那为什么软件工程没有对应的公认标准，以使程序员们可以确信自己的系统是安全、可靠、正确的呢？答案是：这些概念和工具可能还没有 ready for 广泛采纳，但已经经过了数十年的开发了。本书介绍一种特定的工具以及将其应用在完成不同程序验证任务的想法。

由于该文件处于非常早期的草稿阶段，没什么可多说的，所以会直接跳跃至技术材料部分。最终书本此处会添加一些历史的概述和学者引用。目前你可以相信作者，我们正在研究一种很有前途的方法！

学习该书的 common foundation：

• 使用 Coq proof assistant
• 理论方法，证明新 property 时，考虑任何技术中会出现的 four broad elements
  • Encoding：每种编程语言都有语法（syntax）和语义（semantic），前者定义程序的样子，后者定义程序运行时的方式（含义对应的行为）。即使直觉上这些元素看起来很明显，我们经常发现，在定义语法和语义的最高级严密性时，还需要做出令人惊讶的微妙选择。看似微不足道的决定可能会对我们的推证过程产生重大影响。
  • Invariants： 有关程序的每个定理都是由转换系统（transition system）来陈述的，具备一组状态和状态之间的转换关系。关于程序的证明都已通过寻找转换系统的一个不变式（invariants）来进行。不变式概念的地位很接近于数学中的数学归纳法，广为人知且深受喜爱。
  • Abstraction： 一般来说，直接分析转换系统（transition system）太过复杂。我们使用抽象的方式简化成更易理解的 transition system，需证明新的系统保留了原始系统所有的相关属性。
  • Modularity： 还是，针对转换系统的复杂性，我们将其拆成系列模块，再用 well-behaved composition operations 将他们重新组合。抽象和模块化通常时同时进行的。

证明在本书后续章节将很少出现，因为作者认为纸质证明太过时了。对应的，每一章包含一个 Coq 源文件，请在这里面阅读、执行、理解。