程序正確性證明有非形式的與形式的兩種。前者的主要方法叫做“歸納命題法”。這個方法的主要思想是，在一個程序和它的輸人謂詞與輸出謂詞給定後，通過證明一組關於這個程序中的若幹重要變量的命題之間存在著蘊涵關係，來證明這一程序的正確性。我們現在通過一個簡單的例子來說明這一方法。
這是很容易驗證的。最後我們需要證明這個程序不會陷人無窮循環。這也很容易證明。因為每經過一次循環，就變小一些。所以不會出現無窮循環。這就證明了這個程序是正確的。
在這一方法中，原來需要由人找到一組合適的歸納命題。至於這些命題間的蘊涵關係則可以用機器來證明。近年來發現，歸納命題的產生也可以部分自動化。
程序正確性的形式證明是將一個程序的驗證歸納為謂詞演算中一個定理的證明。由於詞演算中的比較簡單的定理的證明是可以利用機器來進行的，程序的形式證明，在理論上是可以完全自動的。但由於目前機器證明中用的證明算法效率很低，在機器上實現的程序的形式證明也是效率很低的。在證明算法方麵出現突破以前，這種形式證明的方法是難以實際應用的。
關於軟件可靠性技術的幾個問題
軟件靠性技術是軟件工程的中心課題之一。這是因為一個大的軟件在交付使用時還包含有許多錯誤。有的發達國家的導彈中心在60年代後發生過多次試射失敗的事故，事後檢查幾乎都是由計算機軟件錯誤造成的。
由於這種情況，西方閑家的一部分軟件作者在1968年和1969年曾接連兩年在軟件工程的國際討論會。在會上不少人認為大的軟件成本很高而可靠性很差，出現了“軟件危機”。“軟件程”這一概念是1968年才提出來的，目的主要是為了解決“軟件危機中體說來就是解決大的軟件可靠性差的問題。許多人認為，如果將其他較成熟的:程領域（包括計算機硬件程)中行之有效的某些方法用到軟件設計中並發展一些軟件設計特有的方法，就能夠有效地提高可靠性。從那時起軟件可靠性技術的研究有了觀的進展。
在今年春天發表的一篇論文中甚至於說，這一方向是注定要失敗的。我們在後麵將討論這個問題。
結構程序設計的思想在最近十年中是程序設計方法論方麵討論最多的題目之一，已在許多地方被采用。近幾年提出的“正確程序技術”可以看作是由結構程序設計思想發展而來的。後者針對大的程序完成後難於驗證的事實，提出要移植其他一些工程部門中用過的應用預製部件的方法，建立一個由經過充分驗證的基本程序塊組成的程序庫，然後依照一些組成規則來構成各種軟件。這一方向是值得重視的。
經過改進的測試方法
最近幾年國外幾個地方同時有人提出了一種新的測試方法。這個方法可以稱作符號測試法。通常的測試法是通過一些輸入取樣來進行測試，如果一個程序對於一些輸人來說，輸出的結果是正確的，這個程序就被認為是正確的。符號測試法的特點在於輸人的可以不是數據而是符號。西方國家有的研究所曾提出過一種符號測試法。這個方法大致如下。
設給定一種程序設計語言。將輸入數據中的數值（如整數)換成符號（用符號來表示輸人是和使用符號的程序變量的名字不一樣的，在執行過程中，一個程序變量可以有許多不同的值，而輸入中的符號則是表示一個未知的但卻是固定的值。）
程序正確性證明
通過嚴格證明來驗證程序正確性的方法，在電子計算機產生後不久就提出來過。1950年明證明了—一個程序的正確性，他的結果發表在英國劍橋大學的一種刊物上。但這方麵的工作整個50年代沒有人繼續去做。到了60年代初期，由於程序驗證的需要益迫切，才又有人進行這方麵的研究，提出了證明程序正確性的方法（這個方法實際上就是50年代用過的方法但這一技術目前還隻能用於較短的程序。
這種證明又分為非形式的證明；形式的證明。下麵我們來看一下這種非形式的證明是怎樣進行的。
60年代提出的方法是非形式證明方法。他們的總的想法是認為，如果把一個程序中各個程序變量在每一步（或特定的某些步）的狀態都記錄下來，並檢查其有無邏輯上不一致之處，就可以查出這一程序是否有邏輯錯誤。如果通過這種方式沒有發現邏輯錯誤，就可以認為這個程序是正確的。
提出的方法大致如下。設在計算開始時，存貯器中每一個單元都存有數。這些數的一個有序序列構成這一-計算的狀態向量，計算機的每一項運算都可以看作是一個狀態向量到另一個狀態向量的變換。所以，程序可以看作狀態向量的函數。這樣程序正確性證明的問題就歸結為遞歸函數論中的一個問題，可以借助遞歸函數論中的一個方法（即遞歸歸納法）加以解決。和裴因特在1967年曾用這個方法證明了一個很簡單的編譯程序的正確性。
推廣了這一方法，將原來的數值向量推廣為符號向量。於是計算機的運算就可以看作是從這種符號狀態向量得出符號表達式的變換。但這一方法是難以實際應用的，因以即使在一個比較短的程序裏也會有太多的表達式。
為了能夠實際應用，必須簡化上述的方法。一個簡化的辦法是隻考慮那些重要變量的交換。這樣，就可以隻考慮狀態向量的元素的一部分，而特定的狀態向量序列就成了一組關於分布在程序中的一些重要變量之間的關係的命題或謂詞。於是驗證程序正確性的過程，就成了證明每一個這樣的命題當程序控製到達這一點時必然成立的過程。這樣的命題稱作歸納斷言（也可以稱作循環謂詞這個方法就稱作歸納斷言法。下麵是一個簡單的例子。中和屯）之間的控製路線構造出一個驗證條件。一條控製路線的驗證條件具有下列的形式