程式設計師從早期程式設計起，就面臨要證明他們的程式達到某種預定目的的任務，這就是程式驗證。早期計算機主要用於數學計算，人們通過對數據的某一子集用人工複雜的簡單過程驗證他們的程式。隨著計算機套用的推廣，程式驗證的任務變得非常困難，這就導致了對基於測試的精巧技術的研究，即它基於電腦程式是一種人工製品，通過實驗過程一定能揭示它的多種屬性這種思想基礎。
基本介紹
- 中文名：程式驗證
- 外文名：Program verification
- 目的：了解程式是否實現了預定的目標
- 提出人：J.諾伊曼
- 提出時間：1947年
- 國別：美籍匈牙利
- 程式驗證方法：調試方法
介紹,基本方法,與驗證的關係,
介紹
程式驗證是指研究程式正確性的理論，即要證明程式達到某種預定目的的任務。
美籍匈牙利科學家J.諾伊曼於1947年發表的論文中就提到程式正確性證明。美國科學家R.W.弗洛依德於1967年系統地提出驗證程式正確性的歸納斷言方法，引起了計算機科學界研究程式驗證的熱潮。英國科學家C.A.R.霍爾於1969年將歸納斷言方法形式化，提出程式驗證的公理系統。1969年以來又陸續出現很多使用歸納斷言方法或者結構歸納法的自動程式驗證系統，其中以70年代中期實現的波伊爾－莫爾程式驗證系統最為著名。70年代以來還出現能輔助用戶正確編製程序的實用的半自動化程式驗證系統。在使用這種系統時，用戶必須協助系統完成程式驗證中創造性最強的部分工作。
基本方法
下面的框圖代表一個非負整數的除法程式。x1是被除數；x2是除數；z1中存放程式加工後得到的商；z2中存放得到的餘數;y1、y2是程式加工時使用的工作單元。START 表示程式的起始，HALT表示程式的終止。方框中是同時賦值語句，如“(y1,y2):=(0,x1)”，表示將y1置0值的同時，將y2的值置為x1。圓框內是測試語句，用於控制程式加工的流程。如框圖中的語句“y2≥x2”，表示當y2的值大於等於x2時，程式按yes的箭頭繼續執行；否則按no的箭頭繼續執行。
為驗證程式，必須首先將程式所要實現的目標形式化,即使用數學公式表達程式加工的初始數據的範圍(稱作輸入謂詞)和程式加工的結果（稱作輸出謂詞）。
若約定各個變數的取值都是整數，上述除法程式的輸入謂詞和輸出謂詞分別為 在用歸納斷言方法證明程式正確性時，還必須在程式的框圖中設定一些數學公式，稱作斷言，表示程式執行到該處時，程式中變數應滿足的數學關係。輸入謂詞可選作起點處的斷言，而輸出謂詞可選作終止點處的斷言。
在除法程式中設定三個斷言，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)均成立。由此推斷公式②是成立的。這樣就完成了對第二條路徑的驗證。對其餘兩條路徑的驗證也是類似的。從而可以證明除法程式的正確性。
歸納斷言方法是由建立斷言和對各條路徑逐條驗證兩部分組成的。建立斷言是一種創造性的工作，而驗證路徑的工作儘管繁瑣，卻是機械的。如何由計算機系統協助用戶歸納出合適的斷言，是程式驗證研究中的重要課題。
用上述方法只能證明在輸入謂詞成立的前提下，程式終止時輸出謂詞一定成立。但不能證明在輸入謂詞成立時，程式一定能終止。不討論程式終止性的程式驗證稱為程式部分正確性的驗證。包括終止性的驗證，則稱為程式完全正確性的驗證。
程式驗證技術除了用於證明程式的正確性，或輔助用戶編制正確程式外，還可從程式正確性角度評價程式設計方法和程式設計語言的優劣。但是，保證程式正確性的有效辦法，不是在編製程序後再去驗證，而是設法在編制過程中，使用適當的技術，使產生的程式是正確無誤的。這類技術叫作程式綜合和程式變形。程式驗證技術和程式綜合變形技術相互參照，共同發展。
與驗證的關係
程式測試是指為了解一個程式是否正確地實現了預定的目標，規定一些初始數據，試驗性地執行這個程式，測試其是否能產生所要的答案，如果發現有誤，就檢查和修改所編的程式，直至對所有規定的初始數據，都能產生預期的結果。但是，程式對不同的初始數據的加工過程是不同的，而初始數據的取值範圍往往又十分廣泛，因此，使用測試方法窮盡程式的各種可能加工過程以確保程式的正確性，幾乎是不可能實現的。因此，測試方法只能發現程式的錯誤，而不能確保程式無誤。而程式驗證則是研究如何使用數學方法嚴格證明一個程式是符合其預定的目標的，因而是正確無誤的。
