形式化方法程序的正確性驗證14

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，即驗證程序對di的執(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)。這種方法的本質就是，用抽象機器的狀態(tài)空間和最簡單的基本指令來定義抽象語言的語義，將抽象語言的程序轉換為一系列抽象機器的基本指令序列。這種對應關是固定的，而且抽象機器的基本指令的含義是固定的，這樣一個程序設計語言的

6、程序就有了一個明確的、無二義的語義。為了驗證一個抽象程序的正確性，就必須在抽象計算機上執(zhí)行其相應的基本指令序列?；局噶钚蛄械囊淮螆?zhí)行只能驗證一組輸入、輸出狀態(tài)之間的關系。因此，用操作語義驗證一個程序的正確性實質上是一種測試型的驗證方式。指稱語義（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ù)學運算公式特征就是其不動點的特征），這些性質是可嚴格推理和證明的。公理語義（axiomatic semantics）公理語義是根據(jù)數(shù)學中的公理化方法形式化程序設計語言相關語法的

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

9、詞，而后置斷言則是該語言成份執(zhí)行后應該滿足的謂詞。有兩種使用公理語義的方式，一種是所謂的自頂向下的方法，用前置和后置斷言描述用戶的需求，然后，將前置斷言向后置斷言轉化的步驟逐步細化，直到每一步都能用計算機語言進行實施為止。只要保證分解的步驟是正確的，那么最終的程序設計結果也是正確的。這種方法的典型代表是唐稚松先生的xyz系列語言4。另一種方法是自底向上的，根據(jù)每個語言單元定義的前置斷言和該成份本身的特征，推導出其后置斷言。一個語法單元的后置斷言可作為下一個語法單元的前置斷言，從而揄出整個程序的后置斷言，以此可證明程序應滿足的性質和程序的正確性。二、公理系統(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!，這一性質可用nÎnfacx=n!命題表示。用命題還可表示程序fac的其它性質，如: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程序的本質是狀態(tài)的轉換，程序的執(zhí)行就是從滿足前置條件的狀態(tài)轉換到滿足后置條件的狀態(tài)，程序的正確性證明即證明2。由于結構化程序設計的任何語法單位均為單入口和單出口的，所以，任何一個結構化的程序設計語言寫的程序均可表示為以下的形式：s1；s2；sn <4>對"d0，存在一個狀態(tài)轉換序列：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)的變化。由于程序的本質是用語句改變程序變量的狀態(tài)，使程序執(zhí)行前的初始狀態(tài)一步一步地變?yōu)橄Ｍ慕K結狀態(tài)的過程，因此，用這種邏輯進行描述程序的性質是不自然的，也是不直觀的。另一個用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)對象的，而程序變化的本質規(guī)律是變量空間狀態(tài)的變化，程序的執(zhí)行是一種動態(tài)現(xiàn)象，所以才產(chǎn)生了上述的困難。hoare邏輯只能描述了某一時刻（當前的）狀態(tài)，而與其它狀態(tài)無關。為了能直接描述程序狀態(tài)變化的本質，我們需要另一種邏輯體系來描述這種隨時間變化而變化的狀態(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)，從而可描述程序的性質，并進行邏輯推導以驗證程序的正確性。下面介紹時態(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表示某個公式或性質）：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，就可論證一程序的性質pp。即只要論證了一個程序p的語義xp，其它的性質均可推出。程序的性質可分為若干層次類型，每種類型可用一個時態(tài)邏輯公式?；蛎枋?，該類型的性質均可用該模式說明，并有一套相關的證明方法。設為狀態(tài)的集合，為所有可能的狀態(tài)序列，那么，一個程序的性質p就是的一個子集。一個時態(tài)公式j說明了一個程

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

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

32、ypersistenceresponseobligationreactivitysafetyguaranteesafety將非安全性的性質稱為進展性。進展性中都包含，它們之間的不同是初始條件和相應的性質發(fā)生的頻率不同。安全性強調(diào)某個要求在計算過程中一直滿足，它可表達某些壞的性質不發(fā)生；而進展性可表示某些好的性質一定會發(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)轉換關系，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)性質，令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)邏輯公式。例如，令：；表示順序算了，即控制自動轉向下一個語句的句首。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邏輯只能驗證一個性質，但不能證明該性質是否與其規(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)邏輯還可證明更復雜的程序性質，如：并行程序的性質、死鎖問題等等。下面對程序的完全正確性證明作補充說明，程序的完全正確性證明2，即在證明程序的部分正確性的同時，也要證明程序能正常結束。由于結構化語言的特殊性，即它只由順序語句、分叉語句和循環(huán)語句等三種類型的語句組成，而順序語句和分叉語句執(zhí)行后一定結束，所以，程序能否結束就是要證明程序中的所有循環(huán)語句能否正確結束。dijkstra為程序的循環(huán)語句的完全正確性證明定義了下面的規(guī)則：（7） i