驗證編寫的程序怎麼驗證

① 程序驗證的基本方法

下面的框圖代表一個非負整數的除法程序。x1是被除數；x2是除數；z1中存放程序加工後得到的商；z2中存放得到的余數;y1、y2是程序加工時使用的工作單元。START 表示程序的起始，HALT表示程序的終止。方框中是同時賦值語句，如(y1,y2):=(O,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)均成立。由此推斷公式②是成立的。這樣就完成了對第二條路徑的驗證。對其餘兩條路徑的驗證也是類似的。從而可以證明除法程序的正確性。
歸納斷言方法是由建立斷言和對各條路徑逐條驗證兩部分組成的。建立斷言是一種創造性的工作，而驗證路徑的工作盡管繁瑣，卻是機械的。如何由計算機系統協助用戶歸納出合適的斷言，是程序驗證研究中的重要課題。
用上述方法只能證明在輸入謂詞成立的前提下，程序終止時輸出謂詞一定成立。但不能證明在輸入謂詞成立時，程序一定能終止。不討論程序終止性的程序驗證稱為程序部分正確性的驗證。包括終止性的驗證，則稱為程序完全正確性的驗證。
程序驗證技術除了用於證明程序的正確性，或輔助用戶編制正確程序外，還可從程序正確性角度評價程序設計方法和程序設計語言的優劣。但是，保證程序正確性的有效辦法，不是在編製程序後再去驗證，而是設法在編制過程中，使用適當的技術，使產生的程序是正確無誤的。這類技術叫作程序綜合和程序變形。程序驗證技術和程序綜合變形技術相互參照，共同發展。