開放邏輯與軟件測試形式化技術(shù)

1、開放邏輯與軟件測試形式化技術(shù)開放邏輯與軟件測試形式化技術(shù) 張偉，張偉，東北大學(xué)信息科學(xué)與工程學(xué)院東北大學(xué)信息科學(xué)與工程學(xué)院主要內(nèi)容主要內(nèi)容 背景知識背景知識 開放邏輯開放邏輯 軟件測試定理軟件測試定理一、一、背景知識背景知識1、人工智能人工智能什么是人工智能（AI的定義）：讓計(jì)算機(jī)去完成需要“智能”才能完成的任務(wù)。人工智能的兩大學(xué)派：符號主義和連接主義：連接主義認(rèn)為思維是大量互連的神經(jīng)元的集體活動所造成的結(jié)果；符號主義則認(rèn)為人類認(rèn)知的基本元素是符號,認(rèn)知過程就是符號表示上的一種運(yùn)算。 符號主義取得了輝煌的成果符號主義取得了輝煌的成果Newell和Simon等人的心理學(xué)小組編制出了一個(gè)稱為邏輯理

2、論機(jī)的數(shù)學(xué)定理證明程序，證明了Russell和Whitehead的“數(shù)學(xué)原理”中的部分定理，并發(fā)現(xiàn)了原書中的幾個(gè)證明錯(cuò)誤。后來的GSP能求解許多問題。計(jì)算機(jī)下棋程序能夠戰(zhàn)勝國際象棋大師。最引人注目的是專家系統(tǒng)。專家系統(tǒng)：一個(gè)軟件系統(tǒng)，其解決某一領(lǐng)域的問題時(shí)，能夠達(dá)到該領(lǐng)域?qū)＜业乃?。如美國斯坦福大學(xué)研制的MYCIN系統(tǒng)，是用于細(xì)菌感染疾病和腦膜炎，然后就如何用抗菌素治療向內(nèi)科醫(yī)生提出醫(yī)療方案，它雖然是最早的專家系統(tǒng)，無論從系統(tǒng)的原理、結(jié)構(gòu)以及性能看都是相當(dāng)成功的。水平穩(wěn)定，知識永存。斯坦福大學(xué)人工智能研究中心(SRI)的地質(zhì)勘探專家咨詢系統(tǒng)PROSPECTOR,可根據(jù)巖石標(biāo)本及其它勘探數(shù)據(jù)，對

3、可能的礦藏進(jìn)行探測。曾發(fā)現(xiàn)過有開采價(jià)值的鋰礦。以上事實(shí)表明，不管是什么領(lǐng)域，只要能夠通過某種知識獲取的手段，把人類專家的某個(gè)專門領(lǐng)域的知識“轉(zhuǎn)移”到計(jì)算機(jī)中去，依靠它的推理程序，計(jì)算機(jī)就有可能作出接近專家水平的工作。從理論上看，符號系統(tǒng)實(shí)際上是公理系統(tǒng)。何為公理系統(tǒng)？ 2.公理系統(tǒng) 歐氏幾何的創(chuàng)始人是公元前三世紀(jì)的古希臘偉大數(shù)學(xué)家歐幾里德。在他以前，古希臘人已經(jīng)積累了大量的幾何知識，并開始用邏輯推理的方法去證明一些幾何命題的結(jié)論。歐幾里德在前人的基礎(chǔ)上，天才般地按照邏輯系統(tǒng)把幾何命題整理起來，構(gòu)建了歐氏幾何系統(tǒng)，建成了一座巍峨的幾何大廈，完成了數(shù)學(xué)史上的光輝著作幾何原本（5+5）：1、從若干不

4、證自明的公理出發(fā)，利用純邏輯推理的方法，證明出所有定理的演繹系統(tǒng)即為公理系統(tǒng)。2、通過有限把握無限；3、第一個(gè)公理系統(tǒng)；4、影響人類文明至今(例如,命題公式集的定義)。 3、數(shù)理邏輯 公理系統(tǒng)的方法延展到邏輯學(xué)的領(lǐng)域，就形成了數(shù)理邏輯。數(shù)理邏輯定義：用數(shù)學(xué)的方法研究邏輯問題。很多推理并不依賴所論證的具體內(nèi)容。如：假如下雨地就會濕。今天下雨了，故今天地濕。人都有一死。蘇格拉底是人，所以蘇格拉底也會死。抽象化后，A B，A B 。形式化的邏輯認(rèn)為，可以用巧妙的方法把推理過程純化，從而不必思考推理中涉及的內(nèi)容，并達(dá)到數(shù)學(xué)那樣的精確性。 萊布尼茲（Leibniz）的理想：把這些思維形式的規(guī)則用符號和數(shù)

5、學(xué)的方式表達(dá)出來，并以數(shù)學(xué)的方式推進(jìn)它，導(dǎo)致了數(shù)理邏輯這門科學(xué)的誕生與發(fā)展。把推理規(guī)則變成演算規(guī)則，萊布尼茲首先創(chuàng)立“邏輯演算”，并且進(jìn)一步設(shè)想，可以設(shè)法造出能進(jìn)行這種演算的機(jī)器，即所謂邏輯機(jī)。萊布尼茲曾幻想過，一個(gè)那樣的黃金時(shí)代即將來臨：兩個(gè)哲學(xué)家發(fā)生哲學(xué)分歧時(shí)，用不著辯論，只要把筆拿在手里，在計(jì)算工具面前坐下來，兩個(gè)人面對面笑嘻嘻地說：“讓我們來計(jì)算一下吧！”誰對誰錯(cuò)，看計(jì)算的結(jié)果就知道了。由此可見，在萊布尼茲看來，“思維”不過是一種復(fù)雜的“計(jì)算”而已。什么是“計(jì)算”？ 通用計(jì)算機(jī)存在性定理被證明 計(jì)算理論在1937年取得了重大的突破。英國學(xué)者圖林(A.M.Turing）發(fā)表了論可計(jì)算的數(shù)

6、及其對判定問題的應(yīng)用。他嚴(yán)格地用數(shù)學(xué)方法定義了什么是“計(jì)算”（能左移、右移、讀、寫的磁帶機(jī)），即著名的“圖靈機(jī)”。還證明了，存在一個(gè)圖靈機(jī)，它能執(zhí)行任何計(jì)算過程，（只要給它所要求計(jì)算過程的程序）通用計(jì)算機(jī)是存在的。這在理論上排除了巴貝奇的繼承者們?nèi)?gòu)造通用計(jì)算機(jī)的疑慮，同時(shí)也為如何構(gòu)造提供了理論指導(dǎo)。（今天計(jì)算機(jī)界沒有Nobel獎，但有Turing獎）。就計(jì)算能力而言，今天的所有計(jì)算機(jī)與TM等價(jià)。 1900年數(shù)學(xué)大會，Hilbert提出了偉大的設(shè)想：建立通用邏輯公理系統(tǒng)，可以囊括所有數(shù)學(xué)定理。同時(shí)提出23個(gè)問題。該設(shè)想最終在1931年被Godel的不完備定理所否定。但是稍小一些的一階邏輯系統(tǒng)含

7、蓋范圍已相當(dāng)強(qiáng)大。后來證明，一階邏輯推理系統(tǒng)（計(jì)算能力）等價(jià)于Turing機(jī)。（TM例） 一階邏輯中的自然推理系統(tǒng)一階邏輯中的自然推理系統(tǒng)G： 自然推理系統(tǒng)推導(dǎo)公式的例子自然推理系統(tǒng)推導(dǎo)公式的例子著名的計(jì)算機(jī)軟件大師 Dijkstra （埃德斯加狄克斯特拉）曾有一段自述, 足以說明數(shù)理邏輯對于計(jì)算機(jī)科學(xué)是何等的重要。（可見，實(shí)現(xiàn)人工智能的邏輯準(zhǔn)備相當(dāng)充分。但是，關(guān)鍵的問題：“什么是智能？”卻一直沒有突破。我們只有著名的圖靈實(shí)驗(yàn)。）二、二、開放邏輯開放邏輯2、OPEN過程模式開放邏輯提出開放邏輯提出OPEN過程模式，其基本工作流程如下：過程模式，其基本工作流程如下：3、版本和版本序列六、事實(shí)反駁

8、與修正演算1、新猜想和新公理2、事實(shí)反駁與極大縮減、事實(shí)反駁與極大縮減當(dāng)一個(gè)形式理論受到事實(shí)反駁時(shí)，人們需要對該形式理論進(jìn)行修正，而修正后所得到的結(jié)果稱為極大縮減。3、R演算演算如果是一個(gè)形式理論，并且 A 可證，那么關(guān)于形式反駁A的極大縮減是與A協(xié)調(diào)的的極大子集合。本節(jié)討論如何求解所有的極大縮減。事實(shí)上，也可以像自然推理系統(tǒng)那樣，設(shè)計(jì)出一組符號演算的規(guī)則，使得對給定的和A，可以使用這些規(guī)則推導(dǎo)出所有的極大縮減。這就是R-演算系統(tǒng)。 4、R演算的例子演算的例子5、R演算的可靠性、完全性演算的可靠性、完全性Reiter的基于模型的診斷推理理論程序修正是軟件開發(fā)過程中一個(gè)相當(dāng)耗費(fèi)時(shí)間的過程。它包括

9、通過測試和模型檢查對程序錯(cuò)誤的定位和糾正。近年來，自動糾錯(cuò)技術(shù)（Automatic debugging)已經(jīng)發(fā)展為軟件工程領(lǐng)域的一個(gè)研究熱點(diǎn)24?；谀Ｐ偷脑\斷技術(shù)是一種被廣泛關(guān)注的程序糾錯(cuò)的人工智能手段。Reiter在1987年提出了著名的診斷推理理論基礎(chǔ)。在他的診斷推理理論中，先將軟件系統(tǒng)表示為邏輯語句集合，而軟件錯(cuò)誤診斷問題被表示為對公式集合一致性測試問題。七、軟件測試和程序修正七、軟件測試和程序修正 ( program debugging ) 的形式化的形式化Reiter的基于模型的診斷推理理論Reiter首先用一階邏輯表示軟件系統(tǒng)和系統(tǒng)的組件。然后給出當(dāng)所有組件都運(yùn)行正常情況下該系統(tǒng)

10、的行為描述。當(dāng)?shù)玫揭唤M該系統(tǒng)實(shí)際運(yùn)行的觀測數(shù)據(jù)（observation ), 就將其與理論期望的行為描述數(shù)據(jù)相比較，如果出現(xiàn)沖突（即，邏輯不一致沖突（即，邏輯不一致（inconsistent），則稱遇到了一個(gè)診斷問題（找到一個(gè)BUG）。程序修正就是要尋找出該系統(tǒng)的哪些組件行為不正常，才導(dǎo)致了這種沖突（和不一致）。這涉及到邏輯語言、系統(tǒng)模型描述、行為描述和系統(tǒng)錯(cuò)誤的形式定義。A system to be diagnosed is given by a triple (SD, COMP,OBS) where SD, the system description, is a set of logic

11、al sentences; COMP, the system components, is a finite set of constants; and OBS, an observation, is a finite set of logical sentences. There is a special predicate AB(c) which says that component c is abnormal。Definition A diagnosis for (SD, COMP,OBS) is a minimal set COMP s.t. the following is con

12、sistent: SDOBSAB(c) | c AB(c) | c COMP .于是，程序診斷問題被轉(zhuǎn)化為一個(gè)邏輯公式的一致性判定問題。EXAMPLE全加器系統(tǒng)的電路全加器系統(tǒng)的電路:全加器系統(tǒng)的全加器系統(tǒng)的SD語句集語句集:該全加器的一次該全加器的一次OBS(發(fā)現(xiàn)錯(cuò)誤發(fā)現(xiàn)錯(cuò)誤):通過求取定義中滿足一致性要求的通過求取定義中滿足一致性要求的找出原因找出原因(BUG):糾錯(cuò)糾錯(cuò):1110001反推反推出錯(cuò)部件出錯(cuò)部件判定性問題：判斷一個(gè)公式集合的一致性是不可計(jì)算的。所以Reiter提出，加上實(shí)際應(yīng)用的限制（如，僅討論線性電路的等價(jià)性問題）來回避一般的一階邏輯公式集合的一致性判斷問題。關(guān)于如何尋找

13、到所有診斷（ diagnosis），一個(gè)直接的辦法是采用生成-測試方法，系統(tǒng)的生成COMP（COMPONENT）的所有子集，然后測試以下公式的一致性： SDOBS AB(c) | c AB(c) | c COMP .后來，Reiter又提出了改進(jìn)效率的方法。* 測試基本定理 開放邏輯十分適合于解決軟件測試與糾錯(cuò)問題：開放邏輯自然的表達(dá)了軟件系統(tǒng)版本的變遷；開放邏輯不需要找出COMP的每個(gè)子集合來一一測試其一致性，而是直接找出導(dǎo)致矛盾（沖突）出現(xiàn)的邏輯前提組件，而且其尋找過程是通過邏輯演算來完成的；開放邏輯可以接受新的事實(shí)（組件）作為其公理（即，接受新的組件做為系統(tǒng)的一個(gè)部分而重新展開推理）。 R演算可以找出最大一致集合因而可以發(fā)現(xiàn)不一致，并且修正程序規(guī)約R演算可以找出最大一致集合：當(dāng)遇到系統(tǒng)的期望行為與實(shí)際測試行為數(shù)據(jù)沖突的時(shí)候，開放邏輯運(yùn)用其R演算來尋找回避這個(gè)沖突的SD+OBS COMP 最大一致集合（等于找到了