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

前言

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

內(nèi)容概要

Coq是一個(gè)用于驗(yàn)證定理的證明是否正確的計(jì)算機(jī)工具?！谕评砗途幊谭矫妫珻oq的語(yǔ)言都擁有足夠強(qiáng)大的能力和表達(dá)能力，可以構(gòu)造簡(jiǎn)單的項(xiàng)，執(zhí)行簡(jiǎn)單的證明，直到建了立完整的理論，學(xué)習(xí)復(fù)雜的算法。　　本書(shū)的主要目：標(biāo)是從實(shí)踐的角度來(lái)理解Coq系統(tǒng)及其基本理論。即歸納構(gòu)造演算。這本書(shū)給出了大量的例子，所有這些例子都可以在計(jì)算機(jī)上執(zhí)行。從本書(shū)配套網(wǎng)站W(wǎng)WW.labri．fr／Perso／～casteran／CoqArl可以下載并執(zhí)行所有證明的例子，而且還提供了書(shū)中200個(gè)練習(xí)的答案?！　∵@本書(shū)是一本很有價(jià)值的教材，它為初學(xué)者提供基礎(chǔ)訓(xùn)練，為有經(jīng)驗(yàn)的人提供必要的專(zhuān)業(yè)知識(shí)，幫助學(xué)習(xí)者開(kāi)發(fā)有實(shí)用價(jià)值的數(shù)學(xué)證明。

作者簡(jiǎn)介

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

書(shū)籍目錄

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

章節(jié)摘錄

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

編輯推薦

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

圖書(shū)封面

圖書(shū)標(biāo)簽Tags

無(wú)

評(píng)論、評(píng)分、閱讀與下載

---

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

---