** * 前言 *

• ###################################################################### *

** * 简介 *

** 本书是一个关于软件基础的课程，它阐明了可靠软件背后的数学根基。

本书的主题包含基本的逻辑概念、计算机辅助定理证明、Coq 证明助理（Proof Assistant）、

函数式编程（Functional Programming）、操作语义（Operational Semantic）、

霍尔逻辑（Hoare Logic）以及静态类型系统（Static Type System）。

本课程的目标受众包括从高级本科生到博士以及研究人员在内的广大读者。

本书并未假定读者有逻辑学或编程语言的背景，不过一定的数学熟练度会很有帮助。

本教程的最大创新之处在于，所有内容百分之百地形式化且通过了机器验证：

所有的文字都是文法上的 Coq 脚本。它旨在与一个 Coq 交互式会话一起阅读。

本书的所有细节都完全用 Coq 形式化了，习题也被设计成用 Coq 来解决。

文件被组织为一系列环环相扣的核心章节，它涵盖了一学期的内容。

“附录”中则包含额外的主题。所有的核心章节都适合高级本科生与研究生。 *

(* ###################################################################### *)

(** * 导论 *)

(** 构建可靠的软件非常难。现代系统的规模，复杂度，参与构建过程的人数，

还有置于系统之上的需求范围，使得构建或多或少正确的软件极为困难，

更不用说百分百正确。同时，由于信息处理继续渗透到社会的各个方面，

程序错误与漏洞的代价越来越严重.

为了应对这些挑战，计算机科学家与软件工程师开发了一系列改进软件质量的方法，

包括对管理软件项目以及编程团队的建议（比如极限编程（Extreme Programming）），

库（比如模型-视图-控制器（Model-View-Controller），发布-订阅（Publish-Subscribe））

以及编程语言（面向对象编程（Object Oriented Programmin），

面向剖面编程（Aspect Oriented Programming），函数式编程（Functional Programming））

的设计哲学，还有用来指定，论证软件属性的数学与工具。

本课程着重于最后一种方法。本书将以下五个概念穿插在一起：

（1）逻辑学中的基本工具，用于构建并证明精确的关于程序的假设；

（2）证明助理用于构建严谨的逻辑论据；

（3）函数式编程思想，同时作为编程方法以及程序与逻辑学之间的桥梁；

（4）用于论证程序属性（例如一个排序函数或编译器满足特定规范）的形式化方法；

以及

（5）类型系统用于建立一个对于某一个编程语言的所有程序都满足的特性

（例如所有类型正确的 Java 程序不能在运行时被破坏）。

这五个主题中的任一个都以其自身方式轻易填满一整个课程，

因此把它们塞在一个课程中自然意味着很多会被遗留在外。

尽管如此，我们仍希望读者会发现这五个主题相得益彰，它们会为读者打下坚实的基础，

使读者可以轻松地深入任一主题。扩展阅读的建议可在 [Postscript] 一章中找到；

所有被引述著作的书目信息可以在 [Bib] 一章中找到。*)

(** ** 逻辑学 *)

(** 逻辑学的研究领域为证明——即对特定命题的真伪性进行不容置疑的论证。

关于逻辑学在计算机科学中作用的资料汗牛充陈。

Manna 以及 Waldinger 称之为“计算机科学的微积分”，而 Halpern 的论文

On the Unusual Effectiveness of Logic in Computer Science 则列出了

逻辑学为计算机科学提供的洞察力和至关重要的工具。的确，他们发现

“事实上，逻辑学在计算机科学中远比在数学中更加有效。

这很值得关注，特别是由于过去一百年来，逻辑学发展的动力大都来自于数学。”

特别来说，归纳证明的基本概念在计算机科学中无处不在。

你以前肯定见过它们，比如说在离散数学或算法分析中。不过在本课程中，

我们会在你未曾所及的深度下对其进行检测。*)

(** ** 证明助理 *)

(** 逻辑学与计算机科学之间的思想交流并不是单方面的：

计算机科学也对逻辑学做出了重要的贡献，

其中之一就是发展了可帮助构造命题/证明的软件工具。

这些工具分为两类：

• 自动化定理证明器提供了一键式操作：它们接受一个命题，

然后返回真、假或超时。

尽管它们的能力仅限于特定种类的推理中，但在近几年却大幅成熟并应用于多种场合，

自动化定理证明器的例子包括 SAT 求解器，SMT 求解器以及 Model Checker。

• 证明助理是一种混合式工具，它能将构建证明中比较常规的部分自动化，

而更困难的部分则依赖于人类解决。

常用的证明助理包括 Isabelle、Agda、Twelf、ACL2、PVS 以及 Coq，还有很多其他的。

本课程围绕 Coq 展开。它是一个自 1983 年以来主要在法国开发的证明助理，

近年来吸引了大量来自研究机构和业界的社区用户。

Coq 为机器验证的形式化论证提供了丰富的环境。Coq 系统的内核是一个简单的证明验证器，

它保证只会进行正确的推论步骤。在此内核之上，Coq 环境提供了高级的证明开发设施，

包括用于半自动化构造证明的强大策略，以及一个包含各种定义和引理的庞大的库。

Coq 已成为各种跨计算机科学和数学研究的关键推动者：

• 作为一个编程语言的建模平台，

Coq 成为了研究员对复杂语言定义进行描述和论证的一个标准工具。

例如，它被用来检查 Java Card 平台的安全性，得到了最高等级的通用准则验证，

它还被用在 x86 和 LLVM 指令集以及 C 之类的编程语言的形式化规范中。

• 作为一个形式化验证软件的开发环境，Coq 被用来构建 CompCert，

一个完全验证过的 C 优化编译器并带有优化，并被用于证明浮点数相关精妙算法的正确性。

Coq 也是 CertiCrypt，一个用于论证密码学算法安全性的环境的基础。

• 作为一个带依赖类型的函数式编程的现实环境，Coq 激发了大量的创新。

例如 Harvard 的 Ynot 项目在 Coq 中嵌入了“关系式霍尔推理”

（一个霍尔逻辑的扩展，我们会在后面看到它）。

• 作为一个高阶逻辑的证明助理，Coq 被用于证实数学中一些重要的结果。

例如 Coq 可在证明中包含复杂计算的能力，使其开发出第一个形式化验证的四色定理证明。

此前数学家们对该证明颇有争议，因为其中一部分用程序对大量组态进行了检查。

在 Coq 的形式化中，所有东西都被检查了，自然包括计算方面的正确性。

近年来，Feit-Thompson 定理在更大的努力下用 Coq 形式化了，

这是对有限单群进行分类的第一大步。

顺便一提，如果你对 Coq 这个名字感到好奇，官方网站给出了他们的解释：

“一些法国计算机科学家有用动物命名软件的传统：像 Caml、Elan、Foc、Phox

都心照不宣地遵循这种默契。在法国，“Coq”是雄鸡，发音也像

Calculus of Constructio 的首字母缩写（CoC），后者是 Coq 的基础。”

高卢雄鸡是法国的象征。C-o-q 还是 Thierry Coquand 名字的前三个字母，

他是 Coq 的早期开发者之一。 *)

(** ** 函数式编程 *)

(** 函数式编程既代表几乎可以在任何编程语言中使用的一系列惯用法，也代表着一族

以这些习惯用法为侧重点设计的编程语言，包括 Haskell、OCaml、Standard ML、F##、

Scala、Scheme、Racket、Common Lisp、Erlang 还有 Coq。

函数式编程已经有数十年历史了--实际上，它甚至可以追溯到 1930

年代 Church 发明的 λ-演算，那时候还没有计算机呢！自 90 年代初以来，

函数式编程激起了业内软件工程师和语言设计者浓厚的兴趣，它还在

Jane St. Capital、Microsoft、Facebook 和 Ericsson

等公司的高价值系统中发挥着关键的作用。

函数式编程最根本的原则是，计算应当尽可能地纯粹，也就是说，

执行代码的唯一效果应当是只产生一个结果：计算应当没有副作用，

即与输入/输出、可变量的赋值、指针重定向等等脱离。

例如，一个命令式的排序函数会接受一个数字列表，通过重组指针使列表得以排序；

而一个纯粹的排序函数则会取一个列表，返回一个含有同样数字，但是已排序的新列表。

这种编程风格最明显的好处之一，就是它能让程序变得更容易理解和论证。

如果对某个数据结构的所有操作都会返回新的数据结构，而旧有的结构没有变动，

那么我们便无需担心它的共享方式，因为程序中一部分的改变并不会破坏另一部分的属性。

在并发程序中，线程间共享的每一个可变状态都是致命 Bug 的潜在来源，

因此这方面的考虑尤为关键。事实上，业界最近对函数式编程的兴趣大部分来源于此，

即它在并发中表现出的简单行为。

人们对函数式编程感到兴奋的另一原因与前文所述的原因相关：

函数式程序通常比命令式程序更容易并行化。

如果一个计算除了产生结果之外没有其它的作用，那么它在何时执行便不再重要。

同样，如果一个数据结构不会被破坏性地修改，那么它可以跨核心或网络地被随意复制。

其实，“映射-归纳”（Map-Reduce）的惯用法就是函数式编程的经典例子，

它在大规模分布式查询处理器（如 Hadoop）中处于核心地位，并被 Google

用来索引整个互联网。

对于本课程而言，函数式编程还有另一个重要的吸引力：

它在逻辑与计算机科学之间架起了一座桥梁。事实上，Coq

本身即可视作一个小巧却有着极强表达能力的函数式编程语言，

以及一组用于陈述和证明逻辑断言的工具的结合体。进而言之，

当我们更加深入地审视它时，会发现 Coq 的这两方面其实基于几乎相同的底层机制

-- 命题即类型，程序即证明，可谓殊途同归。 *)

(** ** 程序验证 *)

(** 本书的前三分之一用于发展逻辑学以及函数式编程的概念框架，提升用

Coq 对非平凡构造进行建模和论证的熟练度。此后，我们会逐渐将重点转移到

对构建可靠软件（和硬件）的事业而言至关重要的两个主题上：

用于证明特定程序具体属性的技巧，以及用于证明整个编程语言共通属性的技术。

对于这两个主题来说，我们首先要找出一种用将程序表示为数学对象的方法，

以此来对二者进行精确的描述，以及用函数或关系表示它们的行为。

对此而言，我们的工具是抽象语法（Abstract Syntax）和操作语义（Operational

Semantics），一种通过编写抽象解释器来指定程序行为的方法。

首先，我们尽量用“大跨步”的方式来产生更加简单可读的操作语义；

之后，我们会转换到更加详细的“小碎步”风格，这样能有效地区分不同种类的“非最终”

程序的行为，这种方式适用于更加广泛的语言特性，包括并发。

我们要仔细考虑的第一个编程语言是 Imp，一个小巧的玩具编程语言，

它包含了传统命令式编程的核心特性：变量、赋值、条件和循环。

我们会学习两种不同的方法来对 Imp 程序的属性进行论证。

首先，若两个 Imp 程序在任何初始内存状态下启动都有相同的行为，

那么我们便认为二者是等价的。这种等价的概念便成为了判定元程序

（操控其它程序的程序，比如编译器和优化器）正确性的标准。

我们会为 Imp 构建一个简单的优化器并证明其正确性。

之后，我们会发展出一套方法论，用于证明特定 Imp 程序的行为是否满足其形式化规范。

我们会介绍霍尔三元组（Hoare triples）的概念：带有前置和后置条件的 Imp

程序描述了在它启动时，存中的什么应当为真；在它终止后，它保证内存中的什么为真。

也会介绍霍尔逻辑（Hoare Logic）的推理原则：一种内建了循环不变式（loop-invariant）

等概念的“领域专用逻辑”，以便对命令式程序进行组合推理。

本课程的这一部分意在让读者尝试各种现实中软件和硬件的证明工作，

以此来获得所需要的关键思想和数学工具。*)

(** ** 类型系统 *)

(** 我们的最后一个主题为类型系统，它覆盖了课程最后的三分之一。

它是一组强大的工具，用于构建给定语言中所有程序的属性。

类型系统是最久经考验、最流行也是最成功的一类形式化验证技术的例子，

它被称作轻量级形式化方法（lightweight formal methods）。

它们是低调而强大的论证技术，以至于自动检查器可以内建在在编译器、

连接器或程序分析器中，而程序员无需熟悉底层理论便可应用。

其它轻量级形式化方法的例子包括硬件和软件的模型检查器、契约检查器，

以及运行时属性监视技术，它用来检测一个系统中某些组件的行为是否遵循规范）。

该主题使得本课程终归圆满：我们在这一部分研究的语言，即简单类型化 λ-演算，

它本质上就是 Coq 核心自身的一个简化模型！ *)

(* ###################################################################### *)

(** ** 扩展阅读 *)

(** 此书旨在自成一体，不过想要对特定主题进行深入研究的读者，可以在 [Postscript]

一章中找到建议的扩展阅读。 *)

(* ###################################################################### *)

(** * 实用指南 *)

(* ###################################################################### *)

(** ** 章节依赖 *)

(** 章节之间的依赖关系以及一些建议的路径图可以在文件[deps.html]中找到。 *)

(* ###################################################################### *)

(** ** 系统需求 *)

(** Coq 可以在 Windows、Linux 和 OS X 上运行。你需要：

• 一个最近的 Coq 安装，可以从 Coq 主页获得。所有内容都能通过 8.4 运行。

（由于 Coq 8.4 和 8.5 之间不兼容的更改，8.5 版本并不适用于本书，）

• 一个能跟 Coq 交互的 IDE。目前为止有两个选项：

• Proof General 是一个基于 Emacs 的 IDE，Emacs 用户应该更喜欢这个。

它需要另外安装（Google 搜索“Proof General”）。

• CoqIDE 是一个更简单的独立 IDE。它随 Coq 一起发布，所以若你已经安装了

Coq，它应该“刚好能用”。它也可以通过对应的依赖来编译安装，

不过在某些平台上还需要额外安装 GUI 库之类的东西。 *)

(* ###################################################################### *)

(** ** 练习 *)

(** 每一章都包含大量的习题。每一个习题都有一个“星级”标记，其意义是：

• 一星：很简单的，强调课程重点的习题。对于大部分读者，一两分钟应该足够了。

养成看到一个就做一个的习惯。

• 二星：直截了当的习题（5 或 10分钟）。

• 三星：需要一点思考的习题（10 分钟到半小时）。

• 四或五星：更困难的习题（半小时以上）。

此外，有些习题被标注为“高阶”，有些习题被标注为“可选”。

只做非高阶和非可选的习题已经能达到对核心概念的不错的覆盖率。

可选习题会提供一点对关键概念的额外练习，以及一些可能会引起读者兴趣的附加主题。

高阶练习留给想要更多挑战（以及对概念更深的理解）的读者。

请勿将习题解答发布在公共位置：Software Foundation

已被广泛地用作自学教程以及大学课程。如果习题答案很容易获得，

那么这本书的效用将大打折扣，对于会为作业打评分的大学课程来说尤其如此。

作者特别请求读者，切勿将习题答案放在任何能够被搜索引擎找到的地方。*)

(* ###################################################################### *)

(** ** 下载 Coq 文件 *)

(** 一个包含“发布版本”的所有笔记的源代码 tar 包

（包含一组 Coq 脚本和 HTML 文件）可在此获得：

<<

http://www.cis.upenn.edu/~bcpierce/sf

本书的中文版可在此获得：

<<

https://github.com/MarisaKirisame/SFCT

如果你是在一个课程中使用这些笔记的，那么你可能有这些文件的本地扩展版，

此时你应当使用它们而非发布的版本。*)

(* ###################################################################### *)

(** * 对授课员的标准 *)

(** 如果你有意用这些课件授课，那么无疑肯定会发现你希望改进或增加的东西。

我们欢迎你的贡献！

为保证情况的清晰和合法性以及单点责任制，任何情况下都不应出现许可条款的的调整，

授权的转移等等，我们要求所有贡献者（即，任何可访问开发者仓库的人）根据

“作者记录”为他们的贡献赋予版权信息如下：

I hereby assign copyright in my past and future contributions

to the Software Foundations project to the Author of Record of

each volume or component, to be licensed under the same terms

as the rest of Software Foundations. I understand that, at

present, the Authors of Record are as follows: For Volumes 1

and 2, known until 2016 as "Software Foundations" and from

2016 as (respectively) "Logical Foundations" and "Programming

Foundations," the Author of Record is Benjamin Pierce. For

Volume 3, "Verified Functional Algorithms", the Author of

Record is Andrew W. Appel. For components outside of

designated Volumes (e.g., typesetting and grading tools and

other software infrastructure), the Author of Record is

Benjamin Pierce.

请您向 Benjamin Pierce 发一封电子邮件，描述一下你自己，

以及你打算如何使用这些课件，内容包括

(1) 以上版权转让协议，以及

(2) 执行 "htpasswd -s -n NAME" 后产生的结果，

其中 NAME 是你偏好的用户名。

我们为你设置 subversion 仓库和开发者邮件列表的访问权限。

在仓库中你会找到一个包含更多指引的 [INSTRUCTORS] 文件。

*)

(* ###################################################################### *)

(** * 翻译 *)

(** 感谢翻译志愿者团队的努力，Software Foundations

有了可以阅读的日文版[http://proofcafe.org/sf]。

中文版正在翻译中。

*)

(** $Date: 2016-05-26 17:51:14 -0400 (Thu, 26 May 2016) $ *)