交互式定理证明与程序开发：Coq归纳构造演算的艺术

基本信息

书名:交互式定理证明与程序开发：Coq归纳构造演算的艺术

定价：59.00元

作者:伯托特

出版社：清华大学出版社

出版日期：2010-1-3

ISBN：9787302208136

字数：690000

页码：432

版次：1

装帧：平装

开本：大16开

内容提要

Coq是一个用于验证定理的证明是否正确的计算机工具。—在推理和编程方面，Coq的语言都拥有足够强大的能力和表达能力，可以构造简单的项，执行简单的证明，直到建了立完整的理论，学习复杂的算法。

本书的主要目：标是从实践的角度来理解Coq系统及其基本理论。即归纳构造演算。这本书给出了大量的例子，所有这些例子都可以在计算机上执行。

这本书是一本很有价值的教材，它为初学者提供基础训练，为有经验的人提供必要的专业知识，帮助学习者开发有实用价值的数学证明。"

目录

1　概述

2　类型和表达式

3　命题和证明

4　依赖积

5　常用逻辑

6　归纳数据类型

7　证明策略和自动化证明

8　归纳谓词

9　函数及其规范

10　程序抽取和命令式程序设计

11　实例分析

12　模块系统

13　无穷对象和证明

14　归纳类型基础

15　一般递归

16　自反证明

序言 IX 1996 年11 月发布的Coq 6.1 版引入了所有上述理论成就，也包括了几项对提高效率有关键作用的技术，特别是Bruno Barras 的规约机制，Christina Cornes 的处理归纳定义的高级证明子。还有Yann Coscoy 的把证明翻译成自然语言（英语和法语）的翻译器，它把证明子构造的证明项用可读的方式表达出来。这是同类证明系统还没有具备的一项重要功能，它使我们能够对形式证明进行检查。在程序验证的领域中，J.-C. Filliatre 在他1999 年的论文中展示了怎样在Coq 中进行命令式程序的证明。他重新采用了Floyd-Hoare-Dijkstra 倡导的在命令式语言中使用断言的方法，命令式程序被看作是从它们的指称语义所获得的函数表达式所对应的记号。Coq 系统是一个两级架构，核心是CoC 验证器。通过在Coq 中对构造演算的元理论进行形式化，可以从验证算法的正确性证明中抽取出验证器，这一点也显示了进行两级架构划分的意义。这是一项出色的技术成果，它在形式化方法的安全性方面迈出了一大步。为了在数学方面做开发工作，Judica.l Courant 在Objective Caml 的模块机制的启发之下，勾画了一个模块语言的基础，这也为库的可重用性和大规模软件验证开辟了道路。新成立的Trusted Logic 公司使用Caml 组和Coq 组的技术进行智能卡系统的正确性验证。这也表明了Coq 研究的价值。其他应用项目也纷纷开始。以后的Coq 系统经历了完全的重新设计，版本7拥有一个函数式核心，主要架构师是Jean-Christophe Filli.tre，Hugo Herbelin 和Bruno Barras 。一个用于tactics 设计的新语言由David Delahaye 开发出来，此后人们可以用高级语言为复杂的证明策略编程。为了对数值软件进行正确性验证，Micaela Mayero 研究了实数的公理化问题。同时，Yves Bertot 重新利用CtCoq 的思想，用Java 语言开发了一个复杂的图形界面PCoq 。2002 年，也就是Judica.l Courant 完成论文之后的第四年，Jacek Chr.aszcz 采用了类似Caml 的方法把模块和函子系统整合在一起。作为理论开发环境中的一个平滑的结合，这一扩展显著地改进了库的通用性。Pieere Letouzey 提供了从证明中提取程序的一个新算法，它把整个Coq 语言都考虑了进去，包括模块系统。在应用方面，Coq 已经足够强壮，并可用作实现特定证明工具的低层语言，比如用于时间自动机模拟和验证的CALIFE 平台，用于命令式程序证明的Why 工具，在欧洲项目VERIFICARD 中开发的用于Java 小应用程序（Java applet ）验证的Krakatoa 工具。这些工具使用Coq 语言描述和证明模型的特性，尤其是在自动工具不能处理的复杂情形，这些工具显得很有用。在经过三年的努力之后，Trusted Logic 成功地完成JavaCard 语言的整个执行环境的形式化模拟。这项安全方面的工作获得EAL7 证书奖（公共标准下最高级别的奖励）。这一形式开发工作使用了121000 行Coq 代码，总共278 个模块。Coq 也被用于开发先进的数学定理库，包括构造性数学和经典数学。在构造性数学领域中工作需要对Coq 的逻辑语言进行限制，以便同数学家常用的公理保持逻辑上的和谐一致。在2003 年底，在经过对主要的输入语言进行重新设计之后发布了8.0 版本，这就是本书中采用的版本。浏览一下Coq 用户群所作的贡献的目录（地址：），读者将清楚地看到在Coq 中已经完成的数学开发工作的丰富性。开发组遵循Boyer 和Moore 提出的要求，在相继发布的Coq 版本之间保持库的兼容性。在必要的时候，提供一些工具把旧的证明脚本自动转换成新的证明脚本，以此确保用户的开发工作不会因新版本的出现而过时。许多这样的库是由Coq 组外的研究人员所开发的，有的在国外，有的在工业界。我们羡慕这个用户群体对Coq 的坚持，他们完成了非常复杂的证明开发。直到今天，使用Coq 总是带有一定的实验性质，尤其是缺乏一个足够全面细致，逐步深入的用户指导书。有了本书，这一需求现在得到了满足。Yves Bertot 和Pierre Castéran 多年以来就是Coq 各个版本的专家级用户。他们是Coq 开发组之外的“客户”，正因为如此，他们并不回避Coq 中的潜在问题。他们也不会宣传一个尚不成熟的的解决方案。他们的所有例子都可以在当前的版本中进行验证。他们所写的这本书以渐进的方式介绍了Coq 系统的所有功能。这一陈述详尽的著作所付出的代价是它的厚度。希望初学者不会因此而后退，书中关于内容难度的指示可以帮助他们在学习时作出适合自己的选择，他们不需要从第一页读到最后一页。这本书可以作为一本参考书来使用。用户可以在长期使用Coq 的过程中，在遇到新困难时来查找解决方案。本书包含了大量精心选择循序渐进的例子，这也是此书比较厚的原因。读者常常愿意自己一步步重做一遍这些例子。事实上，我们也建议读者在读这本书的时候要同时使用一台装有Coq 证明器的计算机，一边看书一边操作书中的例子。这本书所展示的是经过30 年形式化方法研究所积累的成果，该领域的内在难度是不能忽略的，要成为使用Coq 的专家就不得不付出一定的代价。这本书经过了三年的编写和修改，这一过程促使了Coq 中的记号统一化，对证明工具的作用做出更简明的解释，并整理出让非专家也能够理解的出错信息。自然，我们承认以后还会有需要改进之处。愿读者在这个即困难又令人兴奋的世界里的探索获得成功。愿他们的努力能够在完成最后一个QED 时得到满足，这可能需要数周甚至数月的艰苦工作，能够到达终点的人会得到应有的收获。