形式化方法程序的正確性驗(yàn)證14

1、第十四講 形式化方法-程序的正確性驗(yàn)證一、概述計(jì)算機(jī)的程序是一種靜態(tài)的對(duì)象，但它所描述的問題（問題的解）卻是一個(gè)動(dòng)態(tài)的對(duì)象。所謂的程序設(shè)計(jì)就是用程序設(shè)計(jì)語言中的語句改變程序中數(shù)據(jù)對(duì)象的狀態(tài)，構(gòu)造所描述問題的動(dòng)態(tài)行為。這是不自然的，程序所描述的動(dòng)態(tài)行為也無法直接用程序本身的靜態(tài)結(jié)構(gòu)進(jìn)行正確性證明。形式化規(guī)約（formal specification）是需求階段的形式化說明，是用戶需求的嚴(yán)格描述，其一般形式用hoare邏輯描述1如下：p <1>其中和分別表示初始和結(jié)束斷言條件，其含義是：“假如初始狀態(tài)di滿足條件，那么程序結(jié)束并且終結(jié)狀態(tài)df必須滿足”。設(shè)dd1××

2、dn為程序p的狀態(tài)空間，其中，dj(j=1,n)表示程序中數(shù)據(jù)對(duì)象的值域。顯然，由和斷言條件所確定的合法初始和結(jié)束狀態(tài)的集合是d的一個(gè)子集。 執(zhí)行函數(shù)e：×p定義如下： 無定義 對(duì)合法的初始狀態(tài)di，程序p不結(jié)束e（p,di）= 終結(jié)狀態(tài)df 對(duì)合法的初始狀態(tài)di，程序p結(jié)束程序的正確性即為：piff <2>"di(di)(程序p結(jié)束 and (e(p,di)總地來講，驗(yàn)證一個(gè)程序的正確與否有兩種辦法，一種是程序的測試，另一種是程序的正確性證明。1 程序的測試與程序的驗(yàn)證 對(duì)給定的一個(gè)合法的初始狀態(tài)di，當(dāng)程序執(zhí)行結(jié)束時(shí)其終結(jié)狀態(tài)為df，那么，(di)和(df)

3、都應(yīng)該被滿足。這一點(diǎn)可用下式表示：dipdf <3>所謂程序的測試就是驗(yàn)證測試用例dipdf，即驗(yàn)證程序?qū)i的執(zhí)行結(jié)果是否為df。由于合理的初始狀態(tài)是無限的，因此，對(duì)程序驗(yàn)證來講，測試不是一個(gè)完備的方法。測試被認(rèn)為是一種盡量發(fā)現(xiàn)錯(cuò)誤，但并不能保證程序中沒有錯(cuò)誤2的方法。對(duì)大數(shù)應(yīng)用來講，它是可滿足的；但對(duì)有些應(yīng)用來講，測試是一種不能滿足的驗(yàn)證方法，例如：航空、航天等領(lǐng)域的軟件系統(tǒng)。顯然，對(duì)要求絕對(duì)正確的軟件，測試是一種不能采用的方法。無論白盒測試還是黑盒測試都是在無限集合(di,df)|"di,"df, di和df滿足dipdf中選擇有限的一些(di,df)對(duì)進(jìn)

4、行驗(yàn)證，而各種測試方法只是選擇(di,df)的策略不同而已。因此，驗(yàn)證程序是否完全正確要尋求另外的解決途徑。那就是程序的正確性驗(yàn)證。2 形式語義與程序的正確性驗(yàn)證 程序的正確性驗(yàn)證應(yīng)該具有嚴(yán)密的推量過程，以保證程序每步執(zhí)行結(jié)果都是希望的結(jié)果，而與程序執(zhí)行的某個(gè)初始狀態(tài)無關(guān)。程序的正確性證明現(xiàn)有三種方式：操作語義、指稱語義和公理語義。它們分別用不同的形式化方法，嚴(yán)格地證明一個(gè)程序是否正確。盡管這種方法還不夠完善，還不為一般軟件人員所掌握，但它確實(shí)是保證軟件絕對(duì)正確的唯一途徑。操作語義（operational semantics） 操作語義的根據(jù)是，一種程序設(shè)計(jì)語言一但在某種計(jì)算機(jī)系統(tǒng)中實(shí)施，其語

5、義的含義也就完全確定下來了，因此，自然地就用語言的實(shí)施作為語言含義的定義，故稱這種語義為操作語義。當(dāng)然，這種實(shí)施應(yīng)該在一種標(biāo)準(zhǔn)的、抽象的機(jī)器上進(jìn)行。英國科學(xué)家p.j.landin最早提出這種類型的一個(gè)抽象機(jī)器，稱為“棧-環(huán)境-控制-外存”。ibm公司提出了一種可描述程序設(shè)計(jì)語言語義的元語言：vdl。后來，英國的愛丁堡大學(xué)提出了更一般的方法：在數(shù)據(jù)結(jié)構(gòu)上用數(shù)學(xué)關(guān)系建立操作語義的解釋系統(tǒng)。這種方法的本質(zhì)就是，用抽象機(jī)器的狀態(tài)空間和最簡單的基本指令來定義抽象語言的語義，將抽象語言的程序轉(zhuǎn)換為一系列抽象機(jī)器的基本指令序列。這種對(duì)應(yīng)關(guān)是固定的，而且抽象機(jī)器的基本指令的含義是固定的，這樣一個(gè)程序設(shè)計(jì)語言的

6、程序就有了一個(gè)明確的、無二義的語義。為了驗(yàn)證一個(gè)抽象程序的正確性，就必須在抽象計(jì)算機(jī)上執(zhí)行其相應(yīng)的基本指令序列?；局噶钚蛄械囊淮螆?zhí)行只能驗(yàn)證一組輸入、輸出狀態(tài)之間的關(guān)系。因此，用操作語義驗(yàn)證一個(gè)程序的正確性實(shí)質(zhì)上是一種測試型的驗(yàn)證方式。指稱語義（denotational semantics）指稱語義學(xué)認(rèn)為，程序設(shè)計(jì)語言的語義是由其語言成份的語義決定的，而程序設(shè)計(jì)語言成份的語義應(yīng)該是其本身固有的，與程序設(shè)計(jì)語言的個(gè)體實(shí)現(xiàn)無關(guān)。指稱語義的出發(fā)點(diǎn)是語言成份執(zhí)行的最終結(jié)果，而不是其執(zhí)行過程。這種執(zhí)行結(jié)果是由語言成份形式后面隱藏的所指物決定的，故這種方式也稱為指稱語義。指稱語義是由牛津大學(xué)的c.str

7、achey教授創(chuàng)立，d.scott教授完善的，故指稱語義也稱為牛津語義。ibm公司也創(chuàng)立了基于指稱語義的vdm軟件開發(fā)方法。指稱語義的指稱物均為數(shù)學(xué)對(duì)象，如整數(shù)、集合和映射等。指稱物的集合稱為論域。一個(gè)語言的指稱語義就是確定該語言的相關(guān)論域，并給出語法成份到論域上的語義映射。一個(gè)抽象的程序設(shè)計(jì)語言程序的語義就是指稱語義所指的數(shù)學(xué)對(duì)象在論域上的數(shù)學(xué)運(yùn)算，其正確性證明就是指稱語義相應(yīng)的數(shù)學(xué)運(yùn)算公式的特性（遞歸類型語言成份的數(shù)學(xué)運(yùn)算公式特征就是其不動(dòng)點(diǎn)的特征），這些性質(zhì)是可嚴(yán)格推理和證明的。公理語義（axiomatic semantics）公理語義是根據(jù)數(shù)學(xué)中的公理化方法形式化程序設(shè)計(jì)語言相關(guān)語法的

8、語義。賦以公理語義的程序設(shè)計(jì)語言，可推理出該程序設(shè)計(jì)語言的程序語義，也可用邏輯推理的方法證明該程序是否具有某種性質(zhì)。公理語義是最流行的程序證明方法。這種方法最早是由floyd在他的“assigning meanings to programs”一文中提出的，后經(jīng)c.a.hoare在它的“an axiomatic basis for computer programming”一文中發(fā)展和完善的。公理語義對(duì)程序設(shè)計(jì)語言中的每個(gè)成份（包括整個(gè)程序）定義了一對(duì)斷言（assertoin）：前置斷言（precondition）和后置斷言(postcondition)。前置斷言是某個(gè)語言成份在執(zhí)行前滿足的謂

9、詞，而后置斷言則是該語言成份執(zhí)行后應(yīng)該滿足的謂詞。有兩種使用公理語義的方式，一種是所謂的自頂向下的方法，用前置和后置斷言描述用戶的需求，然后，將前置斷言向后置斷言轉(zhuǎn)化的步驟逐步細(xì)化，直到每一步都能用計(jì)算機(jī)語言進(jìn)行實(shí)施為止。只要保證分解的步驟是正確的，那么最終的程序設(shè)計(jì)結(jié)果也是正確的。這種方法的典型代表是唐稚松先生的xyz系列語言4。另一種方法是自底向上的，根據(jù)每個(gè)語言單元定義的前置斷言和該成份本身的特征，推導(dǎo)出其后置斷言。一個(gè)語法單元的后置斷言可作為下一個(gè)語法單元的前置斷言，從而揄出整個(gè)程序的后置斷言，以此可證明程序應(yīng)滿足的性質(zhì)和程序的正確性。二、公理系統(tǒng)：hoare邏輯和時(shí)態(tài)邏輯公理系統(tǒng)是最

10、流行的程序正確性證明和驗(yàn)證的方法，hoare系統(tǒng)是公理系統(tǒng)中的典型代表，它用命題p表法程序p的語義：如果程序執(zhí)行前滿足斷言，則當(dāng)程序執(zhí)行終止后，它一定滿足斷言。下面通過一個(gè)經(jīng)典的例子說明hoare邏輯表述和其優(yōu)缺點(diǎn)。求n!的程序fac（程序fac的描述采用flow語言2，以下其它程序的描述相同）：1=>x; n=>y; (while(y,0) do (*(x,y)=>x; -(y,1)=>y)。表示當(dāng)n為任意自然數(shù)時(shí)，如果該程序執(zhí)行終止，x的值為n!，這一性質(zhì)可用nÎnfacx=n!命題表示。用命題還可表示程序fac的其它性質(zhì)，如:ttfacy=0命題表示無論

11、初值如何，當(dāng)程序終止時(shí)，y的值為0。由于命p不能保證程序p一定能終止，因此，這種命題也稱為程序的部分正確性證明的命題（因?yàn)樽C明程序是否結(jié)束是一個(gè)遞歸不可判定問題，即圖靈機(jī)停機(jī)問題。本文不深入討論，以下所說的程序正確性證明均指部分正確性證明，在文章的最后再給出正確性證明的補(bǔ)充）。這種程序正確性的命題如果為真，就稱其為hoare系統(tǒng)中的定理。那么，如何用公理的方法進(jìn)行推理呢？設(shè)d（a，i）是一個(gè)演繹系統(tǒng)，其中，a（a1，a2，am）表示公理的集合；i（i1，i2，in）表示規(guī)則的集合。公理是一個(gè)系統(tǒng)中不用證明、預(yù)先承認(rèn)的事實(shí)。如果，s是系統(tǒng)中一條合法的語句，那么，s表示s為真，即s是系統(tǒng)中的一個(gè)定

12、理。s1s2spsr表示系統(tǒng)中的一條規(guī)則，其含義是if (s1 and s2 and and sp) then sr。演繹系統(tǒng)中，一個(gè)定理的證明就是一個(gè)合法的語句序列（要用公理或規(guī)則說明為什么該語句是合法的）。下面舉一個(gè)著名的、最簡單的演繹系統(tǒng)及其推理的例子。設(shè)dg=(ag,ig)，其中ag=(a1,a2,a3)為：a1：最少由兩個(gè)點(diǎn)。a2：如果p和q是兩個(gè)不同的點(diǎn)，那么經(jīng)過p和q的線只有一條。a3：假如l是一條線，那么存在一個(gè)不在l上的點(diǎn)。ig=(i1,i2)為：i1： p if p then q qi2： p q p and q下面是“最少有三個(gè)點(diǎn)”的證明步驟：1最少由兩個(gè)點(diǎn) a12存在一

13、條線 1，a2，i13在線外有一個(gè)點(diǎn) 2，a3，i14最少由三個(gè)點(diǎn) 1，2，i2程序的本質(zhì)是狀態(tài)的轉(zhuǎn)換，程序的執(zhí)行就是從滿足前置條件的狀態(tài)轉(zhuǎn)換到滿足后置條件的狀態(tài)，程序的正確性證明即證明2。由于結(jié)構(gòu)化程序設(shè)計(jì)的任何語法單位均為單入口和單出口的，所以，任何一個(gè)結(jié)構(gòu)化的程序設(shè)計(jì)語言寫的程序均可表示為以下的形式：s1；s2；sn <4>對(duì)"d0，存在一個(gè)狀態(tài)轉(zhuǎn)換序列：d1,d2,dn（di表示執(zhí)行語句si后的狀態(tài)）。為了證明<2>，對(duì)每一對(duì)（si, si+1）定義一個(gè)謂詞斷言mi。顯然，可按下面的邏輯推理步驟證明（2）："d0(d0)(d0)m1(d1)m

14、1(d1)m2(d2)mn-1(dn-1)(dn)而證明mi(di)mi+1(di+1)就是證明："di（假如mi(di)，執(zhí)行語句si后，mi+1(di+1)）。這樣，程序的正確性證明就歸結(jié)到每條語句的正確性證明。下面的hoare邏輯為驗(yàn)證程序中的語句提供了一般性的方法。hoare邏輯是這樣的一個(gè)演繹系統(tǒng)dh=(ah,ih),ah是hoare邏輯系統(tǒng)中的公理集（這里不再列出）。ih除了包含一般邏輯系統(tǒng)中的推理規(guī)則外，還包括以下與flow語言有關(guān)的語法語義規(guī)則（公理系統(tǒng)中的一般推理規(guī)則詳見5）：(1)r skip r(2)ra/xa=>x r (3)r s1 o o s2 q

15、rs1；s2 q(4)rÙb s1 q rÙØb s2 q r if b then s1 else s2 q(5)iÙb s i i while b do s iÙØb(6)rr1 r1 s q1 q1q r s q要用hoare邏輯驗(yàn)證一個(gè)程序，即所謂的程序正確性證明（證明hoare系統(tǒng)中的定理），就是用前置條件、邏輯系統(tǒng)中的公理、定理以及上述語言成份所規(guī)定的語義規(guī)則，按程序的執(zhí)行步驟推導(dǎo)出后置條件。下面是應(yīng)用hoare邏輯，對(duì)歸納命題nnfacx=n!的證明過程：1nÎn 前置條件2nÎn Ù l=1

16、 1,Ù+3l=>x; fac的第一條語句4nÎn Ù x=1 2,3,規(guī)則(2)5nÎn Ù x=1 Ù n=n 4, Ù+6n=>y; fac的第二條語句7nÎn Ù x=1 Ù y=n 5,6，規(guī)則(2)8$kÎn(nÎn Ù x=1*n*(n-(k-1) Ù y=n-k) 7É8,令8為規(guī)則5的i9y¹0 6É9，令9為規(guī)則5的b10$kÎn(nÎn Ù x*y=1*n*(n-

17、(k-1)*y Ù y=n-k) 8,911*(x,y)=>x; 循環(huán)的第一條語句12$kÎn(nÎn Ù x=1*n*(n-(k-1)*(n-k) Ù y=n-k) 10,11,規(guī)則213$kÎn(nÎn Ù x=1*n*(n-(k-1)*(n-k) Ù y-1=n-(k+) 12,12É1314-(y,1)=>y; 循環(huán)的第二條語句15$kÎn(nÎn Ù x=1*n*(n-(k-1)*(n-k) Ù y=n-(k+1) 13,14,規(guī)則2

18、16$kÎn(nÎn Ù x=1*n*(n-(k-1) Ù y=n-k) 15É1617i Ù b*(x,y)=>x; -(y,1)=>y; i 10,11,13,14,16,規(guī)則3和618(while¹(y,0) do *(x,y)=>x; -(y,1)=>y) fac的第三條語句19$kÎn(nÎn Ù x=1*n*(n-(k-1) Ù y=n-k) ÙØ (y¹0) 17,18,規(guī)則520x=n! 規(guī)則6，19É20

19、可見，用hoare邏輯進(jìn)行推理與一般的邏輯系統(tǒng)的推理是一樣的。對(duì)flow語言寫的程序，用hoare邏輯證明其正確性的難點(diǎn)是while語句。證明while語句的辦法就是尋找適當(dāng)?shù)难h(huán)不變量(證明某個(gè)循環(huán)語句時(shí)，它的循環(huán)不變量既要利用前面的推理結(jié)果和其它條件，也要為后續(xù)的證明提供必要的前置條件)，其數(shù)學(xué)基礎(chǔ)是不動(dòng)點(diǎn)理論。注意：在證明循環(huán)語句的正確性時(shí)，并不要求循環(huán)不變量在循環(huán)體內(nèi)的證明過程中的每一點(diǎn)上都滿足，它只是要求在循環(huán)體的前和后保持不變即可；另外，不變量在每次循環(huán)前后的形式一樣，但其“含義”是不一樣的，是要發(fā)生變化的。一般情況下，循環(huán)不變量的設(shè)計(jì)是與該循環(huán)的循環(huán)變量相關(guān)的、與循環(huán)體中包含的語

20、句的語義相關(guān)。以hoare邏輯為代表的傳統(tǒng)的公理證明方法的弱點(diǎn)是：程序本身描述的行為是動(dòng)態(tài)的，是隨時(shí)間變化的對(duì)象；而邏輯本身是一個(gè)研究靜態(tài)對(duì)象的數(shù)學(xué)理論，它不能表達(dá)狀態(tài)的變化。由于程序的本質(zhì)是用語句改變程序變量的狀態(tài)，使程序執(zhí)行前的初始狀態(tài)一步一步地變?yōu)橄Ｍ慕K結(jié)狀態(tài)的過程，因此，用這種邏輯進(jìn)行描述程序的性質(zhì)是不自然的，也是不直觀的。另一個(gè)用hoare邏輯進(jìn)行推理的弱點(diǎn)就是推理的方向性。用hoare邏輯驗(yàn)證程序的正確性，就是要構(gòu)造滿足<5>的m1，m2，mn：序列。這就像從入口進(jìn)入迷宮一樣（已知m1），要達(dá)到出口是很難的（尋找mn）。由于有規(guī)則<6>，有人提出了最弱前置

21、條件(weaskest precondition)逆向推理的辦法。其基本思想是：設(shè)一條語句s和一個(gè)該語句執(zhí)行后滿足的斷言q，那么，能使rsq成立的r很多，我們把其中最弱的一個(gè)r記為：wp(s,q)。這樣，我們就可以根據(jù)一個(gè)給定的程序的最后一條語句和程序最終的斷言，倒著一步一步地推出整個(gè)程序唯一的最弱前置條件，記為wp(s,)。設(shè)該程序p的歸納命題的前置斷言為，如果wp(p,)，那么，原命題成立，即它是hoare系統(tǒng)中的一個(gè)定理。按照這一思路，我們也可以設(shè)置相對(duì)應(yīng)的最強(qiáng)后置條件(strongest postcondition):對(duì)給定的語句s和一個(gè)該語句執(zhí)行前滿足的斷言p，能使psq成立的q很多

22、，我們把其中最強(qiáng)的一個(gè)q記為sp(p,s)。對(duì)程序p的hoare邏輯的命題p，從給定程序的第一條語句和程序的前置斷言開始，一步一步地推出整個(gè)程序最后一條語句的最強(qiáng)后置條件，記為：sp(,p)。如果sp(,p)，那么，命題p亦成立。還有一種辦法就是，從前向后推出該程序的前綴¢p的最強(qiáng)后置條件sp(,¢p)；同時(shí)，從后向前推出該程序后綴p¢的最弱前置條件wp(p¢,)。當(dāng)兩個(gè)方向的推理交匯時(shí)，如果sp(,¢p) wp(p¢,)，則命題得證。尋求wp(p,)和sp(,p)在理論經(jīng)上是可行的，但實(shí)際操作起來卻是相當(dāng)困難和費(fèi)時(shí)的。這就使得用ho

23、are邏輯的方法證明程序的正確性有相當(dāng)?shù)碾y度，這主要是因?yàn)閔oare邏輯采用的元語句是命題邏輯，它本身是研究靜態(tài)對(duì)象的，而程序變化的本質(zhì)規(guī)律是變量空間狀態(tài)的變化，程序的執(zhí)行是一種動(dòng)態(tài)現(xiàn)象，所以才產(chǎn)生了上述的困難。hoare邏輯只能描述了某一時(shí)刻（當(dāng)前的）狀態(tài)，而與其它狀態(tài)無關(guān)。為了能直接描述程序狀態(tài)變化的本質(zhì)，我們需要另一種邏輯體系來描述這種隨時(shí)間變化而變化的狀態(tài)信息。時(shí)態(tài)邏輯就是能描述變量隨時(shí)間變化而變化的邏輯系統(tǒng)。顯然，用時(shí)態(tài)邏輯可描述程序的動(dòng)態(tài)語義，而且比較直觀。時(shí)態(tài)邏輯是公理語義的程序正確性證明的一個(gè)分支。時(shí)態(tài)邏輯是由以色列科學(xué)家a.pnueli和z.manna等人創(chuàng)立的，由于在傳統(tǒng)的

24、邏輯中增加了上一時(shí)刻、下一時(shí)刻等算子，使它能描述程序的歷史和將來的狀態(tài)，從而可描述程序的性質(zhì)，并進(jìn)行邏輯推導(dǎo)以驗(yàn)證程序的正確性。下面介紹時(shí)態(tài)邏輯，以及用時(shí)態(tài)邏輯證明程序正確性的方法。設(shè)有窮變?cè)蟰=x1,x2,xn構(gòu)成的變?cè)M的值(x1,x2,xn)為狀態(tài)s，s(xi)表示xi在狀態(tài)s下的值，在一定的上下文中s(xi)可簡寫為xi。同樣，s(e)表示表達(dá)式e在狀態(tài)s下的值（對(duì)表達(dá)式e(xi1,xi2,xim),定義s(e(xi1,xi2,xim)e(s(xi1),s(xi2), s(xim)。令(s0,s1,sk,)為模型，s0表示當(dāng)前狀態(tài)，s1表示下一個(gè)狀態(tài)，等等。在時(shí)態(tài)邏輯中，原子、公式

25、和連接詞Ø、Ù、Ú、É、º以及作用于非時(shí)態(tài)變?cè)?和"與一般的邏輯系統(tǒng)相同5。時(shí)態(tài)連接詞又分為將來(future)和過去(past)兩大類。將來時(shí)態(tài)連接詞及其含義為： next (): (s,j) p iff (s,j+1) phenceforth(): (s,j) p iff "k,k³j (s,k) peventually(): (s,j) p iff $k,k³j (s,k) puntil(m): (s,j) pmq iff $"k,k³j(s,k) q and "i,

26、k>i³j (s,i) punless(w): (s,j) pwq iff (s,j) pmq or (s,j) p(s,j) $u:p iff $s¢,s¢是s的u-變體（s¢，j) p(s,j) "u:p iff "s¢,s¢是s的u-變體（s¢，j) p注：（s，0） p 可簡寫為s p其中，最重要的是o和w，其它的時(shí)態(tài)連接詞均可用他們表示，如： ppwf pØØppmq(pwq)Ùq過去時(shí)態(tài)連接詞也有對(duì)應(yīng)的一組時(shí)態(tài)公式、§、°、和等，詳見6。

27、同其它演繹系統(tǒng)一樣，用時(shí)態(tài)邏輯進(jìn)行演繹的系統(tǒng)可表示為dt=(at,it),at除包括一般邏輯系統(tǒng)中的公理外，還包括以下八條將來公理和八條過去公理：fx0：ppfx1：ØpÛØpfx2：(pq)Û (pq)fx3：(pq)Û (pq)fx4：ppfx5：(pÞp) (pÞp)fx6：pwqÛ(qÚ(pÙ(pwq)fx7：pÞpwqfx8：pÞp八條過去公理不再列出，詳見6。it表示時(shí)態(tài)邏輯演繹系統(tǒng)的規(guī)則（p表示程序，p表示某個(gè)公式或性質(zhì)）：rx1(gen): pp pp rx2

28、(spec): pp pprx3(inst): pp pprx4(mp): p(p1ÙÙpn)q, pp1,ppn pq rx5(p-tau):"p,"p,p是合法的狀態(tài)公式 ppit中還包括其它一些推導(dǎo)出的規(guī)則、量詞規(guī)則和一階謂詞規(guī)則等，詳見6。這些均被稱為一般規(guī)則，還有一類與程序有關(guān)的規(guī)則：rx6(init): qp pp rx7(step): ptq p(pÞq)由以上兩公式還可推出：rx8(s-inv): qp,ptp pp令xp：qÙ(taken (t)ÙdiligentÙjust(t)Ùcom

29、passionate(t)表示程序p時(shí)態(tài)語義， tÎt tÎj tÎc則有如下語義公理： rx9(t-sem): pxp如果xpp，那么：1. pxpp rx52. pxp rx93. pp 1,2,rx4 也就是說，只要證明了pxp，以及在時(shí)態(tài)邏輯系統(tǒng)下的xpp，就可論證一程序的性質(zhì)pp。即只要論證了一個(gè)程序p的語義xp，其它的性質(zhì)均可推出。程序的性質(zhì)可分為若干層次類型，每種類型可用一個(gè)時(shí)態(tài)邏輯公式?；蛎枋?，該類型的性質(zhì)均可用該模式說明，并有一套相關(guān)的證明方法。設(shè)為狀態(tài)的集合，為所有可能的狀態(tài)序列，那么，一個(gè)程序的性質(zhì)p就是的一個(gè)子集。一個(gè)時(shí)態(tài)公式j(luò)說明了一個(gè)程

30、序的性質(zhì)，當(dāng)且僅當(dāng)，"sÎp，sj。時(shí)態(tài)公式的形式不同可反映不同的程序性質(zhì)。安全性(safety properties)所有等價(jià)于p形式的公式被稱為安全公式，它描述的性質(zhì)被稱為安全性。它反映了程序執(zhí)行中某些不變的性質(zhì)。其中一種稱為條件安全性：pq(等價(jià)形式為（°( pÙfirst)q）表明，當(dāng)p滿足計(jì)算模型初態(tài)時(shí)，該計(jì)算模型具有不變的性質(zhì)q。保證性(guarantee properties)所有等價(jià)于p形式的公式被稱為保證公式，它描述的性質(zhì)被稱為程序的保證性。它所映了程序執(zhí)行中一定發(fā)生的性質(zhì)，例如：termial。責(zé)任性(obligation prope

31、rties)所有等價(jià)于ni=1(piÚqi)形式的公式被稱為責(zé)任公式，它描述的性質(zhì)被稱為責(zé)任性。響應(yīng)性(response properties)所有等價(jià)于p形式的公式被稱為響應(yīng)公式，它描述的性質(zhì)被稱為響應(yīng)性。它描述了某些性質(zhì)出現(xiàn)了無數(shù)次。持久性（persistence properties）所有等價(jià)于p形式的公式被稱為持久公式，它描述的性質(zhì)被稱為持久性。它描述了程序中某些最終變穩(wěn)定的性質(zhì)。反應(yīng)性（reactivity properties）所有等價(jià)于pÚp形式的公式被稱為反應(yīng)公式，它描述的性質(zhì)被稱為反應(yīng)性。這些性質(zhì)之間的關(guān)系如下圖所示（連線表示包含關(guān)系）：reactivit

32、ypersistenceresponseobligationreactivitysafetyguaranteesafety將非安全性的性質(zhì)稱為進(jìn)展性。進(jìn)展性中都包含，它們之間的不同是初始條件和相應(yīng)的性質(zhì)發(fā)生的頻率不同。安全性強(qiáng)調(diào)某個(gè)要求在計(jì)算過程中一直滿足，它可表達(dá)某些壞的性質(zhì)不發(fā)生；而進(jìn)展性可表示某些好的性質(zhì)一定會(huì)發(fā)生。程序的部分正確性的時(shí)態(tài)邏輯公式為：（程序結(jié)束）它等價(jià)于：（程序結(jié)束°（first） 6可見程序的部分正確性是一個(gè)安全性問題。要證明6，即要證明6在一個(gè)程序所能訪問的狀態(tài)(p_accessible states)中都是可滿足的。由于程序的可訪問狀態(tài)均是執(zhí)行一個(gè)程序的語

33、句而得到的，因此，6的證明可歸納于程序的語句的證明。 flow語言中各語句的時(shí)誠語義如下：1空語句 （1：skip 1） r1：move (1,1)pres(y)其中，r1表示可能的程序狀態(tài)轉(zhuǎn)換關(guān)系，y表示程序中的所有變量，pres(y)表示集合y的值保持不變。以下相同。 2賦值語句 （1：a=>x 1：） r1：move (1,1) Ù x=a Ù pres(y-x)3條件語句 （1：if c then l1：s1 else l2：s2） r1：rt1Úrf1其中，rt1：move(1,11) Ù c Ù pres(y)rf1：move

34、(1,12) ÙØ c Ù pres(y)4循環(huán)語句 （1：while c do 1：s；1：） r1：rt1Úrf1其中，rt1：move(1,1) Ù c Ù pres(y)rf1：move(1,1) ÙØ c Ù pres(y)即對(duì)一個(gè)程序的語句，按上述規(guī)定的語義，驗(yàn)證一個(gè)p類型的安全性（程序的部分正確性）在變換后還都滿足。即采用如下的規(guī)則（inv_b）：qjjtj j其它的一些規(guī)則也可用于證明程序的正確性，如：mon_i, con_i規(guī)則等。但值得一提的是，一個(gè)程序的部分正確性并非總是可歸納的。例

35、如，7中圖1.2的例子。為此，可采用一個(gè)更強(qiáng)的斷言（inv），增量式（sv_psv）證明等策略。下面用時(shí)態(tài)邏輯驗(yàn)證fac的$kÎn(nÎnÙy=n)(x=1*n*(n-(k-1)Ùy=n-k)性質(zhì)，令p為$kÎn(nÎnÙy=n)(x=1*n*(n-(k-1)Ùy=n-k),下面逐一驗(yàn)證fac的語句：1=>x; n=>y; (while(y,0) do *(x,y)=>x; -(y,1)=>y)。1tp 前提2p 1=>x p y=n不成立，執(zhí)行后x=13p n=>y p 執(zhí)行后

36、y=n，存在k=n使p成立4p*(x,y)=>x p 3Éy¹0，執(zhí)行循環(huán)體的第一條語句，由于y=n-k和 x*y=1*n*(n-(k-1)*y所以，執(zhí)行該語句后 x=1*n*(n-(k-1)*(n-k)。又y=n-k，得y-1=n-(k+1) 所以p成立。5p-(y,1)=>y p 執(zhí)行該語句后y=y-1，由y-1=n-(k+1)得y=n-(k+1)所以 p成立。6p(while¹(y,0) do *(x,y)=>x; -(y,1)=>y) p 4,57p 由規(guī)則inv_b，此時(shí)，循環(huán)結(jié)束=(y,0)，那么k=n，所以x=1*n*1，即x

37、=n!上述的驗(yàn)證方法還沒有脫離一般邏輯系統(tǒng)驗(yàn)證程序的思路，只是驗(yàn)證的具體方式和規(guī)則變了。用時(shí)態(tài)邏輯還有另一種驗(yàn)證正確性的思路：因?yàn)?，時(shí)態(tài)邏輯可以表示狀態(tài)的變化，我們可以把一種適合于馮.諾依曼型計(jì)算機(jī)進(jìn)行計(jì)算的程序設(shè)計(jì)語言翻譯成時(shí)態(tài)邏輯公式。例如，令：；表示順序算了，即控制自動(dòng)轉(zhuǎn)向下一個(gè)語句的句首。ox=a：表法系統(tǒng)中x的值下一個(gè)時(shí)刻為a，而其它變量的值不變。lb=y：表示當(dāng)前執(zhí)行語句的標(biāo)號(hào)為y下面是flow語言翻譯成時(shí)態(tài)邏輯公式的規(guī)則參見4：1：skip 1： lb=1olb=l； 1：a=>x 1: lb=1(olb=lÙx=a)；l：if c then l1: s1 els

38、e l2: s2l：(lb=lÙc) s1)Ú(lb=lÙØc) s2)；l：while c do l: sl： (lb=lÙc) sÙlb=l)Ú(lb=lÙØc) lb=l)；對(duì)一個(gè)用flow語言寫的程序，用上面的規(guī)則將其變換為時(shí)態(tài)邏輯公式的序列。由于flow的語句變成了時(shí)態(tài)邏輯公式，因此可在邏輯系統(tǒng)中，驗(yàn)證該程序是否和其規(guī)范等價(jià)（用hoare邏輯只能驗(yàn)證一個(gè)性質(zhì)，但不能證明該性質(zhì)是否與其規(guī)范等，這是因?yàn)樵趆oare邏輯系統(tǒng)中，一條語句和psq等價(jià)，psq不是邏輯公式，它不能參加邏輯推理）,從而驗(yàn)證相

39、應(yīng)的flow程序的正確性。設(shè)a表示一段程序p的規(guī)范，tl表示p相應(yīng)的一組時(shí)態(tài)邏輯公式，現(xiàn)已有成形的、機(jī)械的方法證明tl a，但無證明atl的自動(dòng)化方法參見4，只能用手工的方法論證。這種方式總的來講是先有程序，然后再根據(jù)它的規(guī)范來驗(yàn)證該程序的正確性。唐稚松先生將其稱為“馬車置于馬的前方”。他認(rèn)為應(yīng)該先有軟件的規(guī)范，然后根據(jù)規(guī)范得到軟件的實(shí)現(xiàn)。他創(chuàng)立了一套基于時(shí)態(tài)邏輯的xyze系統(tǒng)，軟件的規(guī)范（用抽象的xyzae表示）和軟件的實(shí)現(xiàn)（用可執(zhí)行的xyzee表示）都可在同一時(shí)態(tài)邏輯系統(tǒng)下表達(dá)，并且也可表達(dá)即含xyzae，也含xyzee的中間形式的混合描述。這樣，從最初的規(guī)范到最后的可執(zhí)行程序，形成了一個(gè)

40、逐步細(xì)化的時(shí)態(tài)邏輯描述序列：s1，s2，sn只要保證s1是正確的，且si+1si，那么，sn就一定是對(duì)s1的正確實(shí)現(xiàn)。這種逐步求精的思想就是本文最開始提到的自頂向下的方法，它符合軟件工程的一般原理和工程化的需要。用時(shí)態(tài)邏輯還可證明更復(fù)雜的程序性質(zhì)，如：并行程序的性質(zhì)、死鎖問題等等。下面對(duì)程序的完全正確性證明作補(bǔ)充說明，程序的完全正確性證明2，即在證明程序的部分正確性的同時(shí)，也要證明程序能正常結(jié)束。由于結(jié)構(gòu)化語言的特殊性，即它只由順序語句、分叉語句和循環(huán)語句等三種類型的語句組成，而順序語句和分叉語句執(zhí)行后一定結(jié)束，所以，程序能否結(jié)束就是要證明程序中的所有循環(huán)語句能否正確結(jié)束。dijkstra為程序的循環(huán)語句的完全正確性證明定義了下面的規(guī)則：（7） i