Coq是一個用於驗證定理的證明是否正確的計算機工具。—在推理和編程方面，Coq的語言都擁有足夠強大的能力和表達能力，可以構造簡單的項，執行簡單的證明，直到建了立完整的理論，學習複雜的算法。
基本介紹
- 作者：伯托特
- ISBN：9787302208136
- 頁數：432
- 定價：59.00元
- 出版社：清華大學出版社
- 出版時間：2010-1-3
- 裝幀：平裝
- 開本：大16開
基本信息,內容提要,目錄,序言,
基本信息
書名:互動式定理證明與程式開發：Coq歸納構造演算的藝術
版次：1
裝幀：平裝
開本：大16開
內容提要
本書的主要目：標是從實踐的角度來理解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 時得到滿足，這可能需要數周甚至數月的艱苦工作，能夠到達終點的人會得到應有的收穫。
