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

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

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

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

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

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

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

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

8、語義。賦以公理語義的程序設計語言，可推理出該程序設計語言的程序語義，也可用邏輯推理的方法證明該程序是否具有某種性質(zhì)。公理語義是最流行的程序證明方法。這種方法最早是由Floyd在他的“Assigning Meanings to Programs”一文中提出的，后經(jīng)C.A.Hoare在它的“An Axiomatic Basis for Computer Programming”一文中發(fā)展和完善的。公理語義對程序設計語言中的每個成份（包括整個程序）定義了一對斷言（assertoin）：前置斷言（Precondition）和后置斷言(Postcondition)。前置斷言是某個語言成份在執(zhí)行前滿足的謂

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

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

11、初值如何，當程序終止時，y的值為0。由于命P不能保證程序P一定能終止，因此，這種命題也稱為程序的部分正確性證明的命題（因為證明程序是否結束是一個遞歸不可判定問題，即圖靈機停機問題。本文不深入討論，以下所說的程序正確性證明均指部分正確性證明，在文章的最后再給出正確性證明的補充）。這種程序正確性的命題如果為真，就稱其為Hoare系統(tǒng)中的定理。那么，如何用公理的方法進行推理呢？設D（A，I）是一個演繹系統(tǒng)，其中，A（A1，A2，Am）表示公理的集合；I（I1，I2，In）表示規(guī)則的集合。公理是一個系統(tǒng)中不用證明、預先承認的事實。如果，S是系統(tǒng)中一條合法的語句，那么，S表示S為真，即S是系統(tǒng)中的一個定

12、理。S1S2SPSr表示系統(tǒng)中的一條規(guī)則，其含義是if (S1 and S2 and and SP) then Sr。演繹系統(tǒng)中，一個定理的證明就是一個合法的語句序列（要用公理或規(guī)則說明為什么該語句是合法的）。下面舉一個著名的、最簡單的演繹系統(tǒng)及其推理的例子。設Dg=(Ag,Ig)，其中Ag=(A1,A2,A3)為：A1：最少由兩個點。A2：如果P和Q是兩個不同的點，那么經(jīng)過P和Q的線只有一條。A3：假如L是一條線，那么存在一個不在L上的點。Ig=(I1,I2)為：I1： P if P then Q QI2： P Q P and Q下面是“最少有三個點”的證明步驟：1最少由兩個點 A12存在一

13、條線 1，A2，I13在線外有一個點 2，A3，I14最少由三個點 1，2，I2程序的本質(zhì)是狀態(tài)的轉(zhuǎn)換，程序的執(zhí)行就是從滿足前置條件的狀態(tài)轉(zhuǎn)換到滿足后置條件的狀態(tài)，程序的正確性證明即證明2。由于結構化程序設計的任何語法單位均為單入口和單出口的，所以，任何一個結構化的程序設計語言寫的程序均可表示為以下的形式：s1；s2；sn <4>對"d0，存在一個狀態(tài)轉(zhuǎn)換序列：d1,d2,dn（di表示執(zhí)行語句si后的狀態(tài)）。為了證明<2>，對每一對（si, si+1）定義一個謂詞斷言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)）。這樣，程序的正確性證明就歸結到每條語句的正確性證明。下面的Hoare邏輯為驗證程序中的語句提供了一般性的方法。Hoare邏輯是這樣的一個演繹系統(tǒng)Dh=(Ah,Ih),Ah是Hoare邏輯系統(tǒng)中的公理集（這里不再列出）。Ih除了包含一般邏輯系統(tǒng)中的推理規(guī)則外，還包括以下與FLOW語言有關的語法語義規(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邏輯驗證一個程序，即所謂的程序正確性證明（證明Hoare系統(tǒng)中的定理），就是用前置條件、邏輯系統(tǒng)中的公理、定理以及上述語言成份所規(guī)定的語義規(guī)則，按程序的執(zhí)行步驟推導出后置條件。下面是應用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邏輯進行推理與一般的邏輯系統(tǒng)的推理是一樣的。對FLOW語言寫的程序，用Hoare邏輯證明其正確性的難點是while語句。證明while語句的辦法就是尋找適當?shù)难h(huán)不變量(證明某個循環(huán)語句時，它的循環(huán)不變量既要利用前面的推理結果和其它條件，也要為后續(xù)的證明提供必要的前置條件)，其數(shù)學基礎是不動點理論。注意：在證明循環(huán)語句的正確性時，并不要求循環(huán)不變量在循環(huán)體內(nèi)的證明過程中的每一點上都滿足，它只是要求在循環(huán)體的前和后保持不變即可；另外，不變量在每次循環(huán)前后的形式一樣，但其“含義”是不一樣的，是要發(fā)生變化的。一般情況下，循環(huán)不變量的設計是與該循環(huán)的循環(huán)變量相關的、與循環(huán)體中包含的語

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

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

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

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

24、邏輯中增加了上一時刻、下一時刻等算子，使它能描述程序的歷史和將來的狀態(tài)，從而可描述程序的性質(zhì)，并進行邏輯推導以驗證程序的正確性。下面介紹時態(tài)邏輯，以及用時態(tài)邏輯證明程序正確性的方法。設有窮變元集合V=x1,x2,xn構成的變元組的值(x1,x2,xn)為狀態(tài)s，s(xi)表示xi在狀態(tài)s下的值，在一定的上下文中s(xi)可簡寫為xi。同樣，s(e)表示表達式e在狀態(tài)s下的值（對表達式e(xi1,xi2,xim),定義s(e(xi1,xi2,xim)e(s(xi1),s(xi2), s(xim)。令(s0,s1,sk,)為模型，s0表示當前狀態(tài)，s1表示下一個狀態(tài)，等等。在時態(tài)邏輯中，原子、公式

25、和連接詞Ø、Ù、Ú、É、º以及作用于非時態(tài)變元的$和"與一般的邏輯系統(tǒng)相同5。時態(tài)連接詞又分為將來(Future)和過去(Past)兩大類。將來時態(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，其它的時態(tài)連接詞均可用他們表示，如： ppwf pØØppmq(pwq)Ùq過去時態(tài)連接詞也有對應的一組時態(tài)公式、§、°、和等，詳見6。

27、同其它演繹系統(tǒng)一樣，用時態(tài)邏輯進行演繹的系統(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表示時態(tài)邏輯演繹系統(tǒng)的規(guī)則（P表示程序，p表示某個公式或性質(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中還包括其它一些推導出的規(guī)則、量詞規(guī)則和一階謂詞規(guī)則等，詳見6。這些均被稱為一般規(guī)則，還有一類與程序有關的規(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時態(tài)語義， tÎT tÎJ tÎC則有如下語義公理： RX9(T-SEM): PXp如果XPP，那么：1. PXpp RX52. PXp RX93. Pp 1,2,RX4 也就是說，只要證明了PXP，以及在時態(tài)邏輯系統(tǒng)下的XPP，就可論證一程序的性質(zhì)Pp。即只要論證了一個程序P的語義XP，其它的性質(zhì)均可推出。程序的性質(zhì)可分為若干層次類型，每種類型可用一個時態(tài)邏輯公式?；蛎枋?，該類型的性質(zhì)均可用該模式說明，并有一套相關的證明方法。設為狀態(tài)的集合，為所有可能的狀態(tài)序列，那么，一個程序的性質(zhì)P就是的一個子集。一個時態(tài)公式j說明了一個程

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

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

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

33、句而得到的，因此，6的證明可歸納于程序的語句的證明。 FLOW語言中各語句的時誠語義如下：1空語句 （1：skip 1） r1：move (1,1)Pres(Y)其中，r1表示可能的程序狀態(tài)轉(zhuǎ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)即對一個程序的語句，按上述規(guī)定的語義，驗證一個p類型的安全性（程序的部分正確性）在變換后還都滿足。即采用如下的規(guī)則（INV_B）：QjjTj j其它的一些規(guī)則也可用于證明程序的正確性，如：MON_I, CON_I規(guī)則等。但值得一提的是，一個程序的部分正確性并非總是可歸納的。例

35、如，7中圖1.2的例子。為此，可采用一個更強的斷言（INV），增量式（SV_PSV）證明等策略。下面用時態(tài)邏輯驗證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),下面逐一驗證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，此時，循環(huán)結束=(y,0)，那么k=n，所以x=1*n*1，即x

37、=n!上述的驗證方法還沒有脫離一般邏輯系統(tǒng)驗證程序的思路，只是驗證的具體方式和規(guī)則變了。用時態(tài)邏輯還有另一種驗證正確性的思路：因為，時態(tài)邏輯可以表示狀態(tài)的變化，我們可以把一種適合于馮.諾依曼型計算機進行計算的程序設計語言翻譯成時態(tài)邏輯公式。例如，令：；表示順序算了，即控制自動轉(zhuǎn)向下一個語句的句首。Ox=a：表法系統(tǒng)中x的值下一個時刻為a，而其它變量的值不變。LB=y：表示當前執(zhí)行語句的標號為y下面是FLOW語言翻譯成時態(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)；對一個用FLOW語言寫的程序，用上面的規(guī)則將其變換為時態(tài)邏輯公式的序列。由于FLOW的語句變成了時態(tài)邏輯公式，因此可在邏輯系統(tǒng)中，驗證該程序是否和其規(guī)范等價（用Hoare邏輯只能驗證一個性質(zhì)，但不能證明該性質(zhì)是否與其規(guī)范等，這是因為在Hoare邏輯系統(tǒng)中，一條語句和PsQ等價，PsQ不是邏輯公式，它不能參加邏輯推理）,從而驗證相

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

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