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

1、第十四講 形式化方法-程序的正確性驗(yàn)證一、概述計(jì)算機(jī)的程序是一種靜態(tài)的對象，但它所描述的問題（問題的解）卻是一個(gè)動(dòng)態(tài)的對象。所謂的程序設(shè)計(jì)就是用程序設(shè)計(jì)語言中的語句改變程序中數(shù)據(jù)對象的狀態(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ù)對象的值域。顯然，由和斷言條件所確定的合法初始和結(jié)束狀態(tài)的集合是D的一個(gè)子集。 執(zhí)行函數(shù)E：×P定義如下： 無定義 對合法的初始狀態(tài)di，程序P不結(jié)束E（P,dI）= 終結(jié)狀態(tài)df 對合法的初始狀態(tài)di，程序P結(jié)束程序的正確性即為：Piff <2>"di(di)(程序P結(jié)束 and (E(P,di)總地來講，驗(yàn)證一個(gè)程序的正確與否有兩種辦法，一種是程序的測試，另一種是程序的正確性證明。1 程序的測試與程序的驗(yàn)證 對給定的一個(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)是無限的，因此，對程序驗(yàn)證來講，測試不是一個(gè)完備的方法。測試被認(rèn)為是一種盡量發(fā)現(xiàn)錯(cuò)誤，但并不能保證程序中沒有錯(cuò)誤2的方法。對大數(shù)應(yīng)用來講，它是可滿足的；但對有些應(yīng)用來講，測試是一種不能滿足的驗(yàn)證方法，例如：航空、航天等領(lǐng)域的軟件系統(tǒng)。顯然，對要求絕對正確的軟件，測試是一種不能采用的方法。無論白盒測試還是黑盒測試都是在無限集合(di,df)|"di,"df, di和df滿足diPdf中選擇有限的一些(di,df)對進(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í)是保證軟件絕對正確的唯一途徑。操作語義（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ī)器的基本指令序列。這種對應(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é)對象，如整數(shù)、集合和映射等。指稱物的集合稱為論域。一個(gè)語言的指稱語義就是確定該語言的相關(guān)論域，并給出語法成份到論域上的語義映射。一個(gè)抽象的程序設(shè)計(jì)語言程序的語義就是指稱語義所指的數(shù)學(xué)對象在論域上的數(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ā)展和完善的。公理語義對程序設(shè)計(jì)語言中的每個(gè)成份（包括整個(gè)程序）定義了一對斷言（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>對"d0，存在一個(gè)狀態(tài)轉(zhuǎn)換序列：d1,d2,dn（di表示執(zhí)行語句si后的狀態(tài)）。為了證明<2>，對每一對（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邏輯，對歸納命題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)的推理是一樣的。對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í)間變化的對象；而邏輯本身是一個(gè)研究靜態(tài)對象的數(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è)置相對應(yīng)的最強(qiáng)后置條件(strongest postcondition):對給定的語句S和一個(gè)該語句執(zhí)行前滿足的斷言P，能使PSQ成立的Q很多

22、，我們把其中最強(qiáng)的一個(gè)Q記為sp(P,S)。對程序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)對象的，而程序變化的本質(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è)有窮變元集合V=x1,x2,xn構(gòu)成的變元組的值(x1,x2,xn)為狀態(tài)s，s(xi)表示xi在狀態(tài)s下的值，在一定的上下文中s(xi)可簡寫為xi。同樣，s(e)表示表達(dá)式e在狀態(tài)s下的值（對表達(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)變元的$和"與一般的邏輯系統(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)連接詞也有對應(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ì)一定會發(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)即對一個(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)椋瑫r(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)號為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)；對一個(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就一定是對S1的正確實(shí)現(xiàn)。這種逐步求精的思想就是本文最開始提到的自頂向下的方法，它符合軟件工程的一般原理和工程化的需要。用時(shí)態(tài)邏輯還可證明更復(fù)雜的程序性質(zhì)，如：并行程序的性質(zhì)、死鎖問題等等。下面對程序的完全正確性證明作補(bǔ)充說明，程序的完全正確性證明2，即在證明程序的部分正確性的同時(shí)，也要證明程序能正常結(jié)束。由于結(jié)構(gòu)化語言的特殊性，即它只由順序語句、分叉語句和循環(huán)語句等三種類型的語句組成，而順序語句和分叉語句執(zhí)行后一定結(jié)束，所以，程序能否結(jié)束就是要證明程序中的所有循環(huán)語句能否正確結(jié)束。Dijkstra為程序的循環(huán)語句的完全正確性證明定義了下面的規(guī)則：（7） I