錯誤可分為兩類，即①設計中的一致性錯誤和②語言錯誤。前者又有語法錯誤和定時錯誤兩種。這種語法錯誤（如缺少說明或標號等）是和通常的用高級語言寫的程序中的語法錯誤屬於同一類型的，可以借助通常編譯程序中的語法檢查程序來加以排除。定時錯誤則是通常的程序中沒有的。
設計中的語言錯誤需要對照功能描述來加以檢查。提出的方法中，功能描述語言和結構描述語言是分開的。他們認為，如果能使用同一種語言，可能會有很大好處。下麵我們將介紹一種用同一種語言進行功能描述和結構描述的方法。
軟件設計正確性驗證的研究比硬件驗證的研究要早。這方麵已經發展出來的一些方法中有些可以用於硬件設計的驗證。美國有些人正在研究關於計算機係統設計與驗證的統一方法。在這樣一種統一方法中，軟件中已有的一些技術，如結構程序設計和程序正確性證明等都是有用的。他們認為，如果將結構程序設計和程序正確性證明結合起來用，就會有較好的效果。他們還特別指出，要重視形式驗證的方法。他們認為，雖然這種方法在目前用起來很費時間，能應用的範圍也有限，因而許多人對它評價不高，但這一方法是需要的而完全有可能成為一種實用的技術。因為最近的一些研究結果喪明，應用這一-方法時，證明過程的複雜性並不-定是隨著係統複雜性按照指數函數增長的。這樣就有希望對火的係統進驗證。
在第：節中我們將提出一種新的算法，這種算法既可以用來描述計算機硬件，當時以用來描述軟件。這是一種推廣的算法。這種算法是60年代中期最先提出來的。他們將它應用程序和機器的描述。我們這裏提出的是一種經過改進的形式。這是一種“符號行變換算法”。由於計算過程中計算機在任一給定的單位時間的狀態可以表示成一個符號行，而且機器的各種操作可以表示成機器狀態的變遷，因之機器的各種操作可以表示成符號行變換。正是由於這種關係，符號行變換算法可以比較自然地用來描述計算機的結構。這種算法既可以用作機器的結構描述，也可以用作功能描述。
我們將介紹軟件設計正確性驗證方麵已有的三種方法即：①結構程序設計，②高階軟件技術，③程序正確性證明。
叫符法可以在計算機科學中應用。因為可以用它來刻畫計算機，從而可以用作“算機設計語著”，應用於計算機輔助設計。它也以用作程序語的語言理論的數學工具。因為可以認為一個程序的語言是由一種抽象計算機構成的，而一個計算法可以看作是一個抽象計算機。
現在我們來說明如何一個算法來刻畫一種計算機。
於是這一種機器在開始計數時的初始狀態可以表示成下列的符號表達式。這種計算機的係統設計可以用下列的算法加以刻畫。
下麵這個由26條指令組成的算法描述了一種以上述八條指令為其指令係統的通用數字計算機。這個算法不僅描述了這種機器的功能也描述了它的結構。在這一算法中，一般的機器指令每一條需要算法的指令來加以描述，但條件轉移需要六條。
上麵這個由26條指令組成的算法描述了一種指令係統為上述的條指令的二進製--地址的通用數字計算機。這個算法不僅描述了這種機器的功能也描述了它的結構。在這一算法中，第一條指令為從存貯器中取指令，第二條為對指令碼中的運算碼進行譯碼，第三條至第二十六條實現了原來機器的指令係統停機指令以外的七條指令。一般的機器指令每一條需要三條算法的指令來加以描述，但條件轉移需要六條。
算法也可以用來描述程序。現在我們來說明這種描述是怎樣進行的。下麵我們依次說明對賦值語句，條件語句和循環語句等的描述方法。
這種描述實際上是一種解釋，也就是將程序設計語言中的一個語句解釋為算法中的一條或幾條替換規則。這裏隻有賦值語句的解釋稍為麻煩一些，其他語句的解釋都是比較直接的。對於賦值語句我們采用了間接解釋的方法，就是先將一個給定的賦值語句解釋為在一個特定的抽象計算機（例如我們在前麵定義的V中的一串操作，然後再將這一串機器操作表示成一串替換規則。
幾種程序正確性驗證技術
結構程序設計是程序設計的一種新思想，新方法。最早提出這種方法的是？（見他在1963年發表的文章1968年美國的一份計算技術刊物上發表了一封題目叫做《轉向語句是有害的》的公開信，接著他又和其他一些人應用這一方法編了一個小型的操作係統，並在刊物上發表。在這以後，程序設計的這種新方法引起了人們的注意。
有一家世界聞名的計算機公司曾為一家報紙編了一個情報檢索係統在編這個軟件時用了結構程序設計以及其他一些新方法。據說，這個軟件的可靠性較高，在使用了一年的過程中，隻發現了25處錯誤，平均每三千行有一個錯。有的發達國家編製大型軟件用於宇航進用了從程序設計等設計方法，（隻是沒有用“結構程序設計”這個名詞近幾年來結構程序設計這一方法在美國和西歐風行一時。但最近有人指出，許多程序設計工作者對結構程序設計的理解是比較膚淺；這種膚淺的理解所產生的不良後果已經在顯露出來。