程序驗證

程序驗證是指研究程序正確性的理論，即要證明程序達到某種預定目的的任務。

美籍匈牙利科學家約翰·馮·諾依曼於1947年發表的論文中就提到程序正確性證明。美國科學家羅伯特·弗洛伊德於1967年系統地提出驗證程序正確性的歸納斷言方法，引起了計算機科學界研究程序驗證的熱潮。英國科學家託尼·霍爾於1969年將歸納斷言方法形式化，提出程序驗證的公理系統。1969年以來又陸續出現很多使用歸納斷言方法或者結構歸納法的自動程序驗證系統，其中以70年代中期實現的波伊爾－莫爾程序驗證系統最為著名。70年代以來還出現能輔助用户正確編制程序的實用的半自動化程序驗證系統。在使用這種系統時，用户必須協助系統完成程序驗證中創造性最強的部分工作。 ^[1] 

下面的框圖代表一個非負整數的除法程序。x1是被除數；x2是除數；z1中存放程序加工後得到的商；z2中存放得到的餘數;y1、y2是程序加工時使用的工作單元。START 表示程序的起始，HALT表示程序的終止。方框中是同時賦值語句，如“(y1,y2):=(0,x1)”，表示將y1置0值的同時，將y2的值置為x1。圓框內是測試語句，用於控制程序加工的流程。如框圖中的語句“y2≥x2”，表示當y2的值大於等於x2時，程序按yes的箭頭繼續執行；否則按no的箭頭繼續執行。　 ^[1] 

為驗證程序，必須首先將程序所要實現的目標形式化,即使用數學公式表達程序加工的初始數據的範圍(稱作輸入謂詞)和程序加工的結果（稱作輸出謂詞）。

若約定各個變量的取值都是整數，上述除法程序的輸入謂詞和輸出謂詞分別為　在用歸納斷言方法證明程序正確性時，還必須在程序的框圖中設置一些數學公式，稱作斷言，表示程序執行到該處時，程序中變量應滿足的數學關係。輸入謂詞可選作起點處的斷言，而輸出謂詞可選作終止點處的斷言。

在除法程序中設置三個斷言，A處和C處的斷言分別為上述輸入和輸出謂詞，B處斷言為：

(x1=y1x2+y2)&(y2≥0)　 (1)

反映了y1、y2中存放商數和餘數的中間結果值。

驗證程序的正確性，就是證明在程序的任何一種可能的加工過程中所設置的斷言都是成立的。程序的一個加工過程就是框圖中的一個流程。除法程序的所有可能的流程都是由圖上的三條路徑組合而成：由A至B;由B出發回到B;由B至C。這樣，驗證程序的正確性，就是證明對任一條路徑，只要起點的斷言成立，則終點的斷言也成立。

以第二條路徑為例，它是一條環路。要證明下列命題：若程序執行到環路的起點B時，斷言(1)成立，則程序執行一週，再達到B點時，斷言(1)仍然成立。

環行該圈，就是在(y2≥x2)成立的條件下，執行賦值語句：“(y1,y2):=(y1+1,y2-x2)”，而上述語句的執行結果是使 y1的取值為執行前y1的值加1,y2的取值為執行前y2的值與x2的差,其他變量的值不變。為保證執行該賦值語句後斷言(1)仍然成立,就要求將斷言(1)中的y1代為(y1+1),y2代為(y2-x2)後得到的公式在執行該語句前成立。即：

(x1=(y1+1)x2+(y2-x2))&(y2-x2≥0) (2)

在執行上述賦值語句前成立。但已知執行該語句前斷言①和測試條件(y2≥x2)均成立。由此推斷公式②是成立的。這樣就完成了對第二條路徑的驗證。對其餘兩條路徑的驗證也是類似的。從而可以證明除法程序的正確性。 ^[1] 

歸納斷言方法是由建立斷言和對各條路徑逐條驗證兩部分組成的。建立斷言是一種創造性的工作，而驗證路徑的工作儘管繁瑣，卻是機械的。如何由計算機系統協助用户歸納出合適的斷言，是程序驗證研究中的重要課題。 ^[1] 

用上述方法只能證明在輸入謂詞成立的前提下，程序終止時輸出謂詞一定成立。但不能證明在輸入謂詞成立時，程序一定能終止。不討論程序終止性的程序驗證稱為程序部分正確性的驗證。包括終止性的驗證，則稱為程序完全正確性的驗證。 ^[1] 

程序驗證技術除了用於證明程序的正確性，或輔助用户編制正確程序外，還可從程序正確性角度評價程序設計方法和程序設計語言的優劣。但是，保證程序正確性的有效辦法，不是在編制程序後再去驗證，而是設法在編制過程中，使用適當的技術，使產生的程序是正確無誤的。這類技術叫作程序綜合和程序變形。程序驗證技術和程序綜合變形技術相互參照，共同發展。 ^[1] 

程序測試是指為了解一個程序是否正確地實現了預定的目標，規定一些初始數據，試驗性地執行這個程序，測試其是否能產生所要的答案，如果發現有誤，就檢查和修改所編的程序，直至對所有規定的初始數據，都能產生預期的結果。但是，程序對不同的初始數據的加工過程是不同的，而初始數據的取值範圍往往又十分廣泛，因此，使用測試方法窮盡程序的各種可能加工過程以確保程序的正確性，幾乎是不可能實現的。因此，測試方法只能發現程序的錯誤，而不能確保程序無誤。而程序驗證則是研究如何使用數學方法嚴格證明一個程序是符合其預定的目標的，因而是正確無誤的。 ^[1]