交互式定理證明與程序開發(fā)

前言

定理證明是數(shù)學領域中一個古老的分支，它從公理出發(fā)，利用推理規(guī)則為定理尋找證明過程。但是，當我們把數(shù)學定理的手工證明和日常生活中的演繹推理變成一系列能在計算機上自動進行的符號演算的過程和技術時，定理證明就成為當今軟件工程領域中一種非常重要的形式化技術，即定理證明系統(tǒng)。今天，定理證明系統(tǒng)已經(jīng)被廣泛應用于數(shù)學定理證明、協(xié)議驗證以及軟硬件的安全特性驗證等方面，成為人們解決關鍵軟件系統(tǒng)正確性、可信性的重要方法，也是繼模型檢測技術之后未來軟件工程領域的一個重要發(fā)展方向。為了幫助我國廣大科技工作者和學生更好地學習、掌握和應用定理證明系統(tǒng)，我們CEREUS 小組翻譯了《交互式定理證明和程序開發(fā)—–Coq 的藝術: 歸納構(gòu)造演算》一書。選擇翻譯這本書主要基于如下幾點考慮：1. Coq 是目前國際上交互式定理證明領域的主流工具，它基于歸納構(gòu)造演算，有著強大的數(shù)學模型基礎和很好的擴展性，并有完整的工具集。2. Coq 有一支強大的全職研發(fā)隊伍，支持開源，這對于想學習和使用該系統(tǒng)的讀者非常有益。3. 本書的作者一直從事Coq 的研發(fā)，在書中提供了大量的示例和習題，可以幫助讀者更快地掌握Coq，并理解Coq 背后的基礎理論。翻譯從來就不是一件輕松的事，尤其是這種既有很深的理論高度，又有很強的實踐要求的書，翻譯難度就更大了。CEREUS 小組能夠在一年內(nèi)完成本書的翻譯工作，不僅飽含了小組全體成員的辛勤勞動，也得到了國際學術界許多研究人員的幫助。參與本書翻譯工作的是清華大學軟件學院CEREUS 小組，其中第1～8 章由劉柳、周旻、張連怡負責；第9 章由王瑞負責；第10 章和第12 章由張荷花負責；第11 章、第13～14 章由萬海負責；第15～16 章由陳鋼負責；顧明、陳鋼、宋曉宇、荔建琦負責全書的校稿工作。此外，在翻譯這本書的過程中，我們得到了本書作者的全力支持，澳門科技大學張昱，中國科技大學“中科大-耶魯”高可信軟件聯(lián)合研究中心的郭宇、李兆鵬、李勇、王僖和莊重，倫敦大學皇家霍洛威學院的馮揚悅，INRIA的羅正欽等做了本書的審稿工作，在此一并表示感謝。我們希望這本書作為我國研究定理證明系統(tǒng)的一個新起點，能推動中國定理證明系統(tǒng)的發(fā)展，推動我國軟件工程的健康發(fā)展。我們也希望讀者在閱讀本書的過程中，能夠給我們多提意見。我們的聯(lián)系方式是：cereus@tsinghua.edu.cn 。最后，我們要感謝國家自然科學基金委，本書的翻譯工作得到“可信軟件基礎研究”重大研究計劃的支持。前言Coq 是一個用于驗證定理的證明是否正確的計算機工具。這些定理可能涉及到普通數(shù)學、證明理論或程序驗證。我們的主要目標是從實踐的角度來理解Coq 系統(tǒng)及其基本理論：歸納構(gòu)造演算（the Calculus of Inductive Constructions）。因此，這本書中包含了大量的例子，所有這些例子都可以在計算機上執(zhí)行。為了教學目的，一些例子解釋了錯誤或笨拙的用法以及避免這些問題的準則。我們也盡量分解對話（dialogues）以便讀者能夠通過紙筆或直接在Coq 上對其進行重現(xiàn)。有時，我們會給出一些綜合表達式；它們乍看起來讓人生畏，但事實上也是在Coq 證明輔助工具的幫助下得到的。讀者應該在試驗時對它們進行分解、修改、了解其結(jié)構(gòu)，并獲得一種實際的感受。本書有一個相關網(wǎng)站1，讀者可以從該網(wǎng)站下載并執(zhí)行所有證明的例子。我們也提供了書中200 個練習的答案，以備不時之需。這本書及其網(wǎng)站使用的工具都是2004 年初發(fā)布的Coq V82。用戶對Coq 中已證明的定理的信心來自于構(gòu)造演算（Calculus of Inductive Constructions）的性質(zhì)。構(gòu)造演算是一個形式系統(tǒng)。以λ 演算和類型（typing ）的觀點來看，它結(jié)合了邏輯中的一些最新進展。這個演算的主要性質(zhì)已在此處給出，因為我們相信結(jié)合理論和實踐的知識是使用Coq 全部表達能力的一條最好的路徑。在推理和編程方面，Coq 的語言都擁有足夠強大的能力和表達能力。從構(gòu)造簡單的項，執(zhí)行簡單的證明，到建立完整的理論，學習復雜的算法，對讀者能力有著不同層次的需求。按照所需的能力層次，我們對章節(jié)進行了標注：（沒有標注）初次閱讀即可理解，* 中等程度的實踐者可以閱讀，** 有能力掌握復雜的推理和證明程序者可讀，*** 為有興趣探索Coq 形式系統(tǒng)所有可能性的專家預留。練習也有著相同的標注，從基礎的練習（可以在幾分鐘內(nèi)解決）到非常困難的練習（可能需要幾天的思考）。大多數(shù)的練習都是我們研究工作中遇到問題的簡化版本。在這本書的編寫期間，許多人都給了我們熱情的幫助。尤其要感謝Laurence Rideau，她總是非常友好地為我們提供幫助，并且認真地閱讀了從最初草稿到最終版本中的每一個版本。Gérard Huet 和Janet Bertot 在幫助我們改進技術準確性和寫作風格1 www.labri.fr/Perso/～casteran/CoqArt/。2 coq.inria.fr。方面也投入了大量的時間和精力。另外，我們還要特別感謝Gérard Huet 和Christine Paulin-Mohring 為這本書撰寫前言。感謝整個Coq 開發(fā)小組，研制了這么強大的工具。特別是要感謝：Christine Paulin-Mohring 、Jean-Christophe Filliatre 、Eduardo Gimenez 、Jacek Chrz.aszcz 和Pierre Letouzey ，在歸納類型的內(nèi)在一致性、命令式程序表達、co-歸納類型、模塊、抽取方面給我們提供的寶貴見解，此外，他們還為本書編寫了幾頁內(nèi)容和一些例子。除此以外，Hugo Herbelin 和Bruno Barras 和我們一起合作，幫助確保這本書中描述的所有例子都能被實現(xiàn)。這里，還要感謝我們教過和一起工作過的學生，在與他們共同進行實驗的過程中，我們的知識領域也得到了增長。尤其要指出的是，在里昂高師和波爾多第一大學執(zhí)教時，和Davy Rouillard，Antonia Balaa，Nicolas Magaud，Kuntal Das Barman 和Guillaume Dufay 等合作研究解決一些問題后，才逐漸理解本書中描述的一些觀點。許多學生和研究人員花費了時間來閱讀本書的初稿，并把本書作為教學資料使用。他們給我們提供了改進意見，并給出了一些候選的解決方法。我們想在這里感謝那些為我們寶貴的反饋意見的朋友，他們是：Hugo Herbelin 、Jean-Fran.ois Monin 、Jean Duprat Philippe Narbel 、Laurent Théry 、Gilles Kahn 、David Pichardie 、Jan Cederquist、Frédérique Guilhot 、James McKinna 、Iris Loeb 、Milad Niqui 、Julien Narboux 、Solange Coupet-Grimal 、Sébastien Hinderer 、Areski Nait-Abdallah 、Sim.o Melo de Sousa 。除了以上的朋友外，我們各自的科研環(huán)境發(fā)揮了關鍵作用，感謝他們的支持讓這個項目通過。特別要感謝INRIA 的Lemme 與Signes 小組和波爾多第一大學的支持，以及歐洲的Types 工作組為我們提供機會，讓我們能與富有創(chuàng)新精神的年輕研究人員，如Ana Bove，Venanzio Capretta，Conor McBride 見面交流，本書中一些例子的靈感就來源于他們。非常感謝Springer-Verlag 出版社的工作人員，他們的幫助使這本書最終能夠完成，尤其是Ingeborg Mayer 、Alfred Hofman 、Ronan Nugent 、Nicolas Puech 、Petra Treiber 和Frank Holzwarth 。他們的鼓勵，以及在內(nèi)容、編排、編輯和排版等方面的建議是必不可少的。此外，還要感謝KünkelLopka GmbH 的Julia Merz 所設計的藝術品般的封面。Sophia Antipolis Yves Bertot Talence Pierre Castéran 序言Don Knuth 為充實計算機科學基礎而寫下數(shù)卷程序設計名著時，并沒有把他的著作名選為《計算機程序設計科學》，而是叫做《計算機程序設計藝術》。此后，經(jīng)過30 余年的研究，程序設計和算法才成為一門嚴格的科學。類似地，在形式化證明設計領域，目前正在構(gòu)建一個嚴格的基礎。盡管證明論的主要概念可以追溯到20 世紀30 年代的Gentzen 、G.del 和Herbrand，圖靈本人就已表現(xiàn)出對自動構(gòu)造數(shù)學證明的興趣。然而，直到1960 年才首次出現(xiàn)進行一階邏輯自動證明的實驗，即系統(tǒng)地枚舉Herbrand 域。40 年之后，Coq 證明環(huán)境已成為計算邏輯方面一系列探索中的一個最新成果，在某種意義上，它代表了這一領域的當今水平。然而，Coq 的實際使用依然處于一種藝術狀態(tài)，難以掌握、難以改進。Yves Bertot 和Pierre Castéran 的這本書是一本很有價值的教材，它為初學者提供基礎訓練，為有經(jīng)驗的人提供必要的專業(yè)知識，幫助學習者開發(fā)有實用價值的數(shù)學證明。一個簡短的關于Coq 系統(tǒng)歷史的介紹將幫助讀者學習這個軟件以及它所實現(xiàn)的數(shù)學概念。關于基礎概念起源的知識將有助于讀者了解用戶必須掌握的工作機制，構(gòu)造系統(tǒng)模型時的各種觀點，以及在出現(xiàn)問題時的各種可能的處理方案。Gérard Huet 在1970 年開始在自動定理證明方面進行工作，他使用LISP 語言實現(xiàn)了帶等式的一階邏輯證明器SAM。當時的研究水平只是把所有的邏輯命題翻譯成由文字表（帶符號原子公式的析?。┙M成的表（合取式），量化則由Skolem 函數(shù)代替。在這樣的表示方法之下，推理過程被歸結(jié)為基于例化的互補原子公式配對原理（通常稱為合一消解原理），等式則產(chǎn)生出相對于合一（modulo uni.cation ）的單方向重寫。重寫的順序由人為方法決定，既不保證收斂性，也不保證完備性。證明器是黑箱，它們產(chǎn)生出大量的不可讀的邏輯推理結(jié)論。當時的常見情形是輸入一個假設，然后是等待，直到存儲空間用盡。只有在罕見的簡單情形下，證明器才會給出答案。這一災難性狀況當時并沒有得到充分的理解，人們把它看成是不完全性定理帶來的惡魔。然而，復雜性研究很快顯示出，哪怕是在可判定的領域，比如命題演算，自動定理證明也注定要撞上組合爆炸的墻。一個決定性的突破出現(xiàn)在20 世紀70 年代，那是一個系統(tǒng)化方法的實現(xiàn)，它以終結(jié)序指導重寫。這一進展的基礎是Knuth 和Bendix 的奠基性研究工作。Jean-Marie Hullot 和Gérard Huet 在1980 年完成了一個KB 軟件，它以一種自然的方式實現(xiàn)代數(shù)結(jié)構(gòu)的自動判定過程和半可判定過程。同時，歸納證明領域也取得了穩(wěn)步的進展，最著名的工作是Boyer 和Moore 的NQTHM/ACL 系統(tǒng)。另一項有重要意義的進展是把消解技術推廣到高階邏輯，方法是使用Gérard Huet 在1972 年所設計的基于簡單類型理論的合一算法。該算法同Gordon Plotkin 獨立研究的一個方程理論上的通用合一技術本質(zhì)上一致。同時，邏輯學家（Dana Scott ）和理論計算機科學家（Gordon Plotkin 、Gilles Kahn、Gérard Berry ）正在研究可計算函數(shù)的一種邏輯理論（可計算論域），以及有效可用公理化（可計算歸納），目的是為了定義程序語言的語義。當時人們希望用這個理論嚴格地處理可信軟件的設計問題，這樣的設計將采用形式化方法。一個程序相對于它的邏輯規(guī)范的正確性可以用數(shù)學理論中的定理來表達，算法的數(shù)據(jù)和控制結(jié)構(gòu)在數(shù)學理論中進行描述。在愛丁堡大學，Robin Milner 領導的小組在這方面做出了引人注目的工作。他們的一項重要的成就是在1980 年實現(xiàn)了LCF 系統(tǒng)。該系統(tǒng)頗具智慧地引入了用于輔助證明的策略，后者可以用元語言ML 進行編程。公式不再被歸結(jié)到無法理解的子句，用戶可以使用他們的直覺和知識指導系統(tǒng)進行證明，自動證明（預定義的證明策略和用戶使用ML 語言編寫的特定證明策略的結(jié)合）和手工證明混合在一起。哲學家Per MartinL.f 探索了另一條研究路線。這一方向從Brower 開創(chuàng)數(shù)學的構(gòu)造性基礎開始，經(jīng)由Bishop 的構(gòu)造性分析而擴展深化。以此為基礎，Per MartinL.f 在80 年代設計了直覺主義類型理論，為數(shù)學結(jié)構(gòu)的構(gòu)造性公理化提供了一個優(yōu)美的通用框架，而且適合于用作函數(shù)式程序設計的基礎?？的藸柎髮W的Bob Constable 教授認真地繼續(xù)了這一方向的研究，他實現(xiàn)了Nuprl 軟件，用于從形式證明中進行軟件設計。同時，在Gothenburg 的Chalmers 大學的Brengt Nordstr.m 領導的“程序設計方法組”也進行了類似的研究。所有這些研究都依賴于最初由邏輯學家Alongzo Church 所設計的λ 演算記號，這一演算的純粹形式相當于一個用于定義遞歸泛函的語言，它的帶類型的版本相當于高階謂詞演算（即簡單類型理論，它是最初在Whitehead 和Russell 的《數(shù)學原理》中提出的元數(shù)學系統(tǒng)的一個簡單變種）。更進一步，λ 演算可用于表示自然推理中的證明，由此產(chǎn)生了著名的“Curry-Howard 對應關系”，它表示了證明結(jié)構(gòu)的空間與函數(shù)空間的同構(gòu)。λ 演算的這兩個方面實際上已被用于Automath 系統(tǒng)，該系統(tǒng)是在1970 年由Eindhoven 大學的Niklaus de Bruijn 所設計，目的是為了實現(xiàn)數(shù)學的表示。在這個系統(tǒng)中，λ 表達式的類型不再是函數(shù)空間中的簡單的層次結(jié)構(gòu)。實際上，它們能夠表達函數(shù)的輸入變元同函數(shù)的輸出結(jié)果之間的依賴關系。這可以類比于命題演算擴展到一階謂詞演算，在后一種情況下，謂詞的輸入項是它的定義域中的元素。λ 演算的確是證明論中的主要工具。在1970 年，Jean-Yves Girard 證明了分析的一致性，他的證明使用了稱為System-F 的多態(tài)λ 演算中證明的終止性。這一系統(tǒng)被推廣到一個表示多態(tài)泛函的Fω 系統(tǒng)，因而可為一類超出了傳統(tǒng)序數(shù)層次的算法進行編碼。1974 年，John Reynolds 在推廣ML 語言的受限制的多態(tài)結(jié)構(gòu)時，又重新發(fā)現(xiàn)了這一系統(tǒng)。20 世紀80 年代早期，在邏輯和計算機科學的前沿，類型理論獲得長足進展。在1982 年，Gérard Huet 聯(lián)合巴黎高等師范學院的Guy Cousineau 和Pierre-Louis Curien 在INRIA Rocquencourt 實驗室啟動了Formel 項目。這個小組在LCF 系統(tǒng)的啟發(fā)之下，準備設計和開發(fā)一個更強的證明系統(tǒng)，尤其重要的是，他們準備把ML 語言不僅用于定義tactics，同時用于實現(xiàn)整個系統(tǒng)。這一項在函數(shù)式方面的研究和開發(fā)工作在序言VII 幾年后產(chǎn)生了CAML 語言族，最終導致了今天的Objective Caml 語言，它就是現(xiàn)在的Coq 證明器的實現(xiàn)語言。1984 年，Gilles Kahn 在Sophia Antipolis 組織了一個類型理論的國際會議，在會上，Thierry Coquand 和Gérard Huet 展示了一個把依賴類型和多態(tài)類型綜合在一起的系統(tǒng)，它把MartinL.f 的構(gòu)造性理論融入了Automath 系統(tǒng)的一個擴展，該系統(tǒng)命名為構(gòu)造演算（Calculus of Constructions）。Thierry Coquand 在博士論文中提供了對這一系統(tǒng)的λ 演算基礎的元理論分析。他給出了這一演算終止性的證明，進而給出了關于該演算的邏輯可靠性的證明。這一演算就成了Formel 項目的證明系統(tǒng)的邏輯基礎，Gérard Huet 對這個演算CoC 做出了第一個驗證器，稱為“構(gòu)造引擎”（Constructive Engine) 。1985 年4 月，在Eurocal 會議上演示了在這個驗證器上進行的幾個形式化數(shù)學的開發(fā)工作。這就是Coq 系統(tǒng)的第一階段：一個λ 表達式的類型驗證器，在這個系統(tǒng)中，λ 表達式表示邏輯系統(tǒng)的證明項，或者是數(shù)學對象的定義。這個證明助手的核心是與證明綜合工具完全獨立的，后者的用途是構(gòu)造需要驗證的項，構(gòu)造引擎的解釋器是一個確定性的程序。Thierry Coquand 實現(xiàn)了序列（Sequent ）風格的證明綜合算法，它提供了一組類似LCF 系統(tǒng)的證明策略，支持逐步求精方式構(gòu)造證明項。Coq 第二階段的開發(fā)由Christine Mohring 完成，在Coq 系統(tǒng)中首次實現(xiàn)Prolog 風格的證明搜索，即著名的Auto tactic。這可以看成是今天的Coq 系統(tǒng)的正式誕生。在現(xiàn)在的版本中，Coq 核心依然重新檢查用戶調(diào)用tactic 所構(gòu)造的證明項。這一架構(gòu)有一個附加的優(yōu)點，即簡化了證明搜索的機制，它實際上忽略了類型系統(tǒng)分層所要求的某些約束。Formel 組很快意識到構(gòu)造演算可用于綜合出帶有證書的程序（certi.ed program）， 這一機制與Nuprl 系統(tǒng)的做法相似。一個關鍵點是利用了多態(tài)類型的優(yōu)勢，把一個代數(shù)結(jié)構(gòu)用F 系統(tǒng)的類型表示出來，比如整數(shù)，這里系統(tǒng)性地利用了B.hm 和Berarducci 所提出的方法。Christine Mohring 專注于這一問題，她實現(xiàn)了一個復雜的tactic，在構(gòu)造演算中綜合出歸納原理。以此為基礎，她在1986 年6 月舉行的“計算機科學中的邏輯”（LICS）會議上展示了一種開發(fā)帶證明算法的形式化方法。然而，當她完成了博士論文之后，她意識到她所使用的impredicative 編碼并不遵從常規(guī)模式，即把歸納類型的項限制在類型構(gòu)造子的復合。多態(tài)λ 演算的編碼引入了寄生項，因而不能表示合適的歸納原理。這個部分的失敗實際上給了Christine Mohring 和Thierry Coquand 一個動力，促使他們在1988 年設計了“歸納構(gòu)造演算”，這是原來系統(tǒng)的一個擴展，增加了歸納數(shù)據(jù)類型上的算法的公理化的一些良好的性質(zhì)。Formel 小組在理論研究和系統(tǒng)實驗兩方面始終保持著小心的平衡。他們用模型來評價各種建議的可行性，用原型來驗證系統(tǒng)的能力是否可以擴展到處理實際的證明，他們提供免費的配備了良好的庫和手冊的越來越完整的系統(tǒng)，并努力在各版本之間維持兼容性。這個小組開發(fā)的CoC 原型系統(tǒng)轉(zhuǎn)變成Coq 系統(tǒng)，通過網(wǎng)上論壇發(fā)布的方式把該軟件提供給感興趣的用戶。同時，基礎問題的研究也從不忽略。比如Gilles Dowek 系統(tǒng)性地研究了合一理論和類型論中的證明搜索，這為以后的Coq 發(fā)展提供了堅實的基礎。1989 年，Coq 4.1 版本發(fā)布，該版首次加入了由Benjamin Werner 所設計的從證明中抽取函數(shù)式程序（Caml 語法）的機制。此外，還有一組新的進行自動證明的tactics，以及一個小的數(shù)學和計算機科學方面的知識庫。這一進展標志著一個新階段（new era ）的開始。Thierry Coquand 在Gothenburg 獲得了一個教學的位置，Christine Paulin-Mohring 加入了位于里昂的高等師范學院。此后，Coq 組的工作就在里昂和Rocquencourt 兩地繼續(xù)進行。同時，一個稱為Cristal 的新項目開始了，它的主要課題是圍繞函數(shù)式語言ML 展開研究工作。在Rocquencourt，剛在NuPRL 組完成了經(jīng)典邏輯的構(gòu)造性解釋的博士論文的Chet Murthy 為Coq 帶來了他的新貢獻，在Coq 5.8 版本中引入了更復雜的體系結(jié)構(gòu)。在歐洲支持的一項基礎研究國際項目“邏輯框架”（Logical Framework） 下開始了國際合作研究，三年之后，又在“類型”項目之下繼續(xù)進行。幾個小組同時在稱為“證明助手”（Proof assistant ）的證明工具方面進行開發(fā)，他們之間相互激勵，分享經(jīng)驗。Coq 是這些證明工具中的一個。其他的“證明助手”有：愛丁堡大學的Randy Pollack 開發(fā)的LEGO 系統(tǒng)，劍橋大學的Larry Paulson 開發(fā)的Isabelle 系統(tǒng)，該系統(tǒng)后來由慕尼黑大學的Tobias Nipkow 繼續(xù)，此外，還有Gothenburg 小組開發(fā)的Alf 系統(tǒng)等等。1991 年推出的Coq 5.6 版提供了進行數(shù)學描述的統(tǒng)一語言（Gallina“vernacular”）， 原始歸納類型，從證明中抽取程序的機制，和一個圖形化用戶界面。這使Coq 成為一個可以有效使用的系統(tǒng)，并由此開始了同工業(yè)界的有成效的合作，尤其是同CNET 和Dassault-Aviation 的合作。由于出現(xiàn)了第一批學術界之外的用戶，促使Coq 組寫出了一個教學講義和使用手冊，此時Coq 的使用藝術對于新手依然神秘。Coq 依舊是一個研究性探索的工具和展開實驗的場所。在Sophia Antipolis，Yves Bertot 在原來的Centaur 項目基礎上開發(fā)了CTCoq 界面中的結(jié)構(gòu)操作，使該系統(tǒng)能夠利用鼠標進行交互式證明構(gòu)造，這一技術稱為“Proof-by-pointing”，即用戶通過鼠標點擊來調(diào)用tactics。在里昂，Catherine Parent 的博士論文研究了證明中抽取程序的問題，并把該問題轉(zhuǎn)換成另一個問題，把加入不變式注解的程序作為它們自身正確性證明的框架。在波爾多，Pierre Castéran 的工作顯示這一技術可被用于構(gòu)造具有continuation 語義風格的帶證明（certi.ed）算法庫。在里昂，Eduardo Giménez 在他的博士論文中表明，能夠以繼承性（hereditarily）方式定義有限結(jié)構(gòu)的歸納類型的框架可以被擴展到一個co-inductive 類型的框架，后者可用于對無限結(jié)構(gòu)公理化。作為一個推論，他開發(fā)了涉及數(shù)據(jù)流操作的通訊協(xié)議的證明，這樣就為通訊方面的應用打開了一條路。在Rocquencourt，Samuel Boutin 在他的博士論文中研究了Coq 中自反推理的實現(xiàn)，這一技術在基于代數(shù)重寫的自動證明中有重要的應用。他的Ring tactic 可用于簡化多項式表達式，從而隱式地實現(xiàn)常用的算術表達式代數(shù)操作。另外一些判定過程也顯著地改進了Coq 系統(tǒng)的自動證明能力：比如在Presburger 算術中使用的Omega （由CNET-Lannion 的Pierre Crégut 開發(fā)），在命題演算中使用的Tauto 和Intuition （由Rocquencourt 的César Muňoz 開發(fā))。沒有收縮規(guī)則（contraction ）的謂詞演算中使用的Linear（由里昂的Jean-Christophe Filliatre 開發(fā)）。Amokrane Sa.bi 引入了表達繼承和隱式強制（coercion ）的子類型的概念，這些概念可用于在廣義代數(shù)中進行模塊化證明開發(fā)，尤其是可以簡練地表達范疇論的主要概念。序言IX 1996 年11 月發(fā)布的Coq 6.1 版引入了所有上述理論成就，也包括了幾項對提高效率有關鍵作用的技術，特別是Bruno Barras 的規(guī)約機制，Christina Cornes 的處理歸納定義的高級證明子。還有Yann Coscoy 的把證明翻譯成自然語言（英語和法語）的翻譯器，它把證明子構(gòu)造的證明項用可讀的方式表達出來。這是同類證明系統(tǒng)還沒有具備的一項重要功能，它使我們能夠?qū)π问阶C明進行檢查。在程序驗證的領域中，J.-C. Filliatre 在他1999 年的論文中展示了怎樣在Coq 中進行命令式程序的證明。他重新采用了Floyd-Hoare-Dijkstra 倡導的在命令式語言中使用斷言的方法，命令式程序被看作是從它們的指稱語義所獲得的函數(shù)表達式所對應的記號。Coq 系統(tǒng)是一個兩級架構(gòu)，核心是CoC 驗證器。通過在Coq 中對構(gòu)造演算的元理論進行形式化，可以從驗證算法的正確性證明中抽取出驗證器，這一點也顯示了進行兩級架構(gòu)劃分的意義。這是一項出色的技術成果，它在形式化方法的安全性方面邁出了一大步。為了在數(shù)學方面做開發(fā)工作，Judica.l Courant 在Objective Caml 的模塊機制的啟發(fā)之下，勾畫了一個模塊語言的基礎，這也為庫的可重用性和大規(guī)模軟件驗證開辟了道路。新成立的Trusted Logic 公司使用Caml 組和Coq 組的技術進行智能卡系統(tǒng)的正確性驗證。這也表明了Coq 研究的價值。其他應用項目也紛紛開始。以后的Coq 系統(tǒng)經(jīng)歷了完全的重新設計，版本7擁有一個函數(shù)式核心，主要架構(gòu)師是Jean-Christophe Filli.tre，Hugo Herbelin 和Bruno Barras 。一個用于tactics 設計的新語言由David Delahaye 開發(fā)出來，此后人們可以用高級語言為復雜的證明策略編程。為了對數(shù)值軟件進行正確性驗證，Micaela Mayero 研究了實數(shù)的公理化問題。同時，Yves Bertot 重新利用CtCoq 的思想，用Java 語言開發(fā)了一個復雜的圖形界面PCoq 。2002 年，也就是Judica.l Courant 完成論文之后的第四年，Jacek Chr.aszcz 采用了類似Caml 的方法把模塊和函子系統(tǒng)整合在一起。作為理論開發(fā)環(huán)境中的一個平滑的結(jié)合，這一擴展顯著地改進了庫的通用性。Pieere Letouzey 提供了從證明中提取程序的一個新算法，它把整個Coq 語言都考慮了進去，包括模塊系統(tǒng)。在應用方面，Coq 已經(jīng)足夠強壯，并可用作實現(xiàn)特定證明工具的低層語言，比如用于時間自動機模擬和驗證的CALIFE 平臺，用于命令式程序證明的Why 工具，在歐洲項目VERIFICARD 中開發(fā)的用于Java 小應用程序（Java applet ）驗證的Krakatoa 工具。這些工具使用Coq 語言描述和證明模型的特性，尤其是在自動工具不能處理的復雜情形，這些工具顯得很有用。在經(jīng)過三年的努力之后，Trusted Logic 成功地完成JavaCard 語言的整個執(zhí)行環(huán)境的形式化模擬。這項安全方面的工作獲得EAL7 證書獎（公共標準下最高級別的獎勵）。這一形式開發(fā)工作使用了121000 行Coq 代碼，總共278 個模塊。Coq 也被用于開發(fā)先進的數(shù)學定理庫，包括構(gòu)造性數(shù)學和經(jīng)典數(shù)學。在構(gòu)造性數(shù)學領域中工作需要對Coq 的邏輯語言進行限制，以便同數(shù)學家常用的公理保持邏輯上的和諧一致。在2003 年底，在經(jīng)過對主要的輸入語言進行重新設計之后發(fā)布了8.0 版本，這就是本書中采用的版本。瀏覽一下Coq 用戶群所作的貢獻的目錄（地址：http://coq.inria.fr/contribs/summary.html），讀者將清楚地看到在Coq 中已經(jīng)完成的數(shù)學開發(fā)工作的豐富性。開發(fā)組遵循Boyer 和Moore 提出的要求，在相繼發(fā)布的Coq 版本之間保持庫的兼容性。在必要的時候，提供一些工具把舊的證明腳本自動轉(zhuǎn)換成新的證明腳本，以此確保用戶的開發(fā)工作不會因新版本的出現(xiàn)而過時。許多這樣的庫是由Coq 組外的研究人員所開發(fā)的，有的在國外，有的在工業(yè)界。我們羨慕這個用戶群體對Coq 的堅持，他們完成了非常復雜的證明開發(fā)。直到今天，使用Coq 總是帶有一定的實驗性質(zhì)，尤其是缺乏一個足夠全面細致，逐步深入的用戶指導書。有了本書，這一需求現(xiàn)在得到了滿足。Yves Bertot 和Pierre Castéran 多年以來就是Coq 各個版本的專家級用戶。他們是Coq 開發(fā)組之外的“客戶”，正因為如此，他們并不回避Coq 中的潛在問題。他們也不會宣傳一個尚不成熟的的解決方案。他們的所有例子都可以在當前的版本中進行驗證。他們所寫的這本書以漸進的方式介紹了Coq 系統(tǒng)的所有功能。這一陳述詳盡的著作所付出的代價是它的厚度。希望初學者不會因此而后退，書中關于內(nèi)容難度的指示可以幫助他們在學習時作出適合自己的選擇，他們不需要從第一頁讀到最后一頁。這本書可以作為一本參考書來使用。用戶可以在長期使用Coq 的過程中，在遇到新困難時來查找解決方案。本書包含了大量精心選擇循序漸進的例子，這也是此書比較厚的原因。讀者常常愿意自己一步步重做一遍這些例子。事實上，我們也建議讀者在讀這本書的時候要同時使用一臺裝有Coq 證明器的計算機，一邊看書一邊操作書中的例子。這本書所展示的是經(jīng)過30 年形式化方法研究所積累的成果，該領域的內(nèi)在難度是不能忽略的，要成為使用Coq 的專家就不得不付出一定的代價。這本書經(jīng)過了三年的編寫和修改，這一過程促使了Coq 中的記號統(tǒng)一化，對證明工具的作用做出更簡明的解釋，并整理出讓非專家也能夠理解的出錯信息。自然，我們承認以后還會有需要改進之處。愿讀者在這個即困難又令人興奮的世界里的探索獲得成功。愿他們的努力能夠在完成最后一個QED 時得到滿足，這可能需要數(shù)周甚至數(shù)月的艱苦工作，能夠到達終點的人會得到應有的收獲。 

內(nèi)容概要

Coq是一個用于驗證定理的證明是否正確的計算機工具?！谕评砗途幊谭矫?，Coq的語言都擁有足夠強大的能力和表達能力，可以構(gòu)造簡單的項，執(zhí)行簡單的證明，直到建了立完整的理論，學習復雜的算法?！　”緯闹饕浚簶耸菑膶嵺`的角度來理解Coq系統(tǒng)及其基本理論。即歸納構(gòu)造演算。這本書給出了大量的例子，所有這些例子都可以在計算機上執(zhí)行。從本書配套網(wǎng)站W(wǎng)WW.labri．fr／Perso／～casteran／CoqArl可以下載并執(zhí)行所有證明的例子，而且還提供了書中200個練習的答案。　　這本書是一本很有價值的教材，它為初學者提供基礎訓練，為有經(jīng)驗的人提供必要的專業(yè)知識，幫助學習者開發(fā)有實用價值的數(shù)學證明。

作者簡介

作者：(德國)伯托特(Yves Bertot) (德國)卡斯特蘭(Pierre Casteran) 譯者：顧明 等

書籍目錄

1　概述2　類型和表達式3　命題和證明4　依賴積5　常用邏輯6　歸納數(shù)據(jù)類型7　證明策略和自動化證明8　歸納謂詞9　函數(shù)及其規(guī)范10　程序抽取和命令式程序設計11　實例分析12　模塊系統(tǒng)13　無窮對象和證明14　歸納類型基礎15　一般遞歸16　自反證明附錄參考文獻

章節(jié)摘錄

插圖：Coqf381是一個定理證明輔助工具，學生、研究人員和工程人員可以使用它來表達規(guī)范說明（specification），開發(fā)滿足規(guī)范說明的程序。 Coq非常適合于開發(fā)那些在電信、運輸、能源和銀行等領域需要絕對可信的程序，這些領域中的程序需要嚴格地符合規(guī)范說明，需要對這些程序進行形式化的驗證。在本書中，我們將看到Coq這樣的定理證明輔助工具如何使這一工作變得簡單。Coq系統(tǒng)不僅可以用來開發(fā)安全程序，還可以被數(shù)學家用來開發(fā)證明。Coq系統(tǒng)提供一種具有很強表達能力的邏輯，通常被稱為高階邏輯（higher'-0rder，logic：）。證明以交互的方式進行開發(fā)，并盡可能地借助自動搜索工具的幫助。Coq的應用領域也很廣泛，比如，在邏輯、自動機理論、計算語言學和算法學中都有涉及（參見111）。Coq系統(tǒng)亦可被用作一個邏輯框架。在該框架下，我們可以為新的邏輯提供公理，并基于這些邏輯來開發(fā)證明。比如，我們可以使用∞口為模態(tài)邏輯、時序邏輯、面向資源的邏輯等邏輯系統(tǒng)開發(fā)推理系統(tǒng)，也可以為命令式程序開發(fā)推理系統(tǒng)。計算機輔助定理證明工具是一個大家族，除Coq之外，還有很多享有盛譽的工具，那就是可以從證明中牛成可靠的程序和模塊。在這一章里，我們將非形式化地介紹Coq的主要特性。嚴格的定義和準確的符號將在后而的章節(jié)中給出。這里，我們僅使用一些在數(shù)學或程序設計語言中常用的符號。1.1表達式、類型和函數(shù)Coq的規(guī)范說明語言Gallina可以描述程序設計語言中的常用類型和程序。一個標識符的類型通常由聲明（declaration）和一些規(guī)則來描述.后者使用類型規(guī)則從較簡單的類型出發(fā)構(gòu)造復合類型，每個類型規(guī)則表達了類型的子部分同類型的整體結(jié)構(gòu)之間的聯(lián)系。例如，給定與集合Z相對應的整數(shù)類型z，已知常量一6的類型是整數(shù)，若聲明一個類型為z的變量z，則表達式－6z也是整數(shù)類型z的。但是，給定一個bool常量true，表達式“true×－6”就不是一個合法的表達式。在Gallina語言中，除整數(shù)類型z和布爾類型 bool之外，存在各種各樣的類型。我們經(jīng)常會使用自然數(shù)類型nat，它是包含常數(shù)0和調(diào)用后繼函數(shù)所得到的值的最小類型。

編輯推薦

《交互式定理證明與程序開發(fā)：Coq歸納構(gòu)造演算的藝術》：過程感知的信息系統(tǒng)軟件測試：跨越整個軟件開發(fā)生命周期軟件測試實踐：成為一個高效能的測試專家機器視覺算法與應用數(shù)值方法（c++描述）web技術UML安全系統(tǒng)開發(fā)

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    交互式定理證明與程序開發(fā) PDF格式下載

---