究竟什麼是結構程序設計,有著不同的說法。有人曾將結構程序設計定義為這樣的一種方法,借助這個方法可以使得在測試的每一階段中,需要測試的情形的數目減到很少,從而可以對所有的情形進行測試。另外有人則將它定義為能使得編出來的程序容易懂,容易檢查和容易修改的設計方法。目前,還沒有一個普遍接受的定義。
現在我們來看一下結構程序設計究竟有一些什麼特點。一般認為結構程序設計有下列的兩個特點:①層次結構,②對用到的控製結構的種類作適當的限製,如限製轉向語句的使用,從而使得編出來的程序能夠少犯邏輯錯誤和容易修改。
下列兩組控製結構都是不用轉向語句的。在理論上,第一組控製結構已經足夠,增加三種結構的第二組控製結構效率要提高不少。還有,重要的是要限製控製結構中那些容易產生邏輯錯誤的結構,而這樣的結構非僅限於轉向語句。另一方麵,轉向語句也不一定在所有情形中都會使程序變得晦澀難懂,而且有時不用轉向語句會嚴重影響效率,在這種情形中還是應該用轉向語句。看來對轉向語句的使用隻能限製,而不能完全禁止。
高階軟件技術
如前所述,有的國家為開展宇航事業在60年代後期編製有關軟件時,已經用了模塊式程序設計以及從頂向下程序設計等概念。後來他們在設計外行星往返飛船的軟件時,不僅應用了結構程序設計而且發展出來了一種他們稱之為“高階軟件”的新技術。這種技術在一定意義上可以看作是結構程序設計的推廣。高階軟件是遵守一組形式規則,用軟件的元語言寫出來的軟件(他們將這種形式規則稱作“公理”)。這些規則之中有的是和限製使用轉向語句直接有關的,在這一意義上,結構程序設計可以看作是高階軟件技術的一種特殊情形。
高階軟件技術的基本思想可大致說明如下。
一個形式的控製係統是這樣的一個係統,在其中每一個模塊都可以唯一地表示成下列的形式
定理一個函數匸不能調用另一個調用函數。上述定理可以看作是一條禁止惡性循環的規則。這條規則和數學基礎中為了避免“悖論”而提出的禁止惡性循環的法則十分相似。這一技術的要點就是,針對程序的控製結構中造成一般的邏輯錯誤的原因,找出一組規則,編出來的程序都是遵守這組規則的,從而能避免一般的邏輯錯誤。上述這條禁止惡性循環的規則就是這樣的規則。因為在允許一個函數可以調用它自己時,容易導致邏輯錯誤,是就製定了這一規則。
高階軟件技術是一種避免程序中的邏輯錯誤的方法,它與數學基礎中提出過的一些避免“邏輯悖論”的方法有很多相似之處。原來提出高階軟件這一技術的人也是意識到了這一點的。他們中間的有些人曾指出,有的軟件錯誤與“漢悖論”相似,而上述定理與提出的禁止惡性循環的法則相似。另外有人曾指出,等人從程序設計中去掉轉向語句的主張與直覺主義者從邏輯推理中去掉排中律的主張有類似之處。實際上還有更多相似的地方。通過形式證明來驗證程序正確性的方法與隻學派企圖通過無矛盾性證明來保證數學中沒有邏輯矛盾的思想顯然有類似之處。高階軟件技術作為一種公理方法也可以認為是在方法論方麵與公理集合論有相通之處。
由於軟件技術中避免邏輯錯誤的問題與數學基礎中避免悖論的問題是同一類的邏輯問題,數學基礎過去幾十年中在這方麵積累起來的經驗包括失敗的經驗,如隻方案的破產:對於軟件可靠技術可能是有參考價值的。
程序正確性證明
通過嚴格證明來驗證程序正確性的思想,在電子計算機產生後不久就有人提出來過。1950年時曾有人證明方法驗證了一個程序的正確性,並發表了這一證明。但由於早期還沒有很大的程序,這方麵的需要不甚迫切,在相當長的時間裏沒有人繼續從事這方麵的工作。到了60年代中期,出現了第三代計算機之後,由於一些程序的結構日趨複雜,程序的可靠性問題變得愈來愈尖銳。為了解決這個問題,人們就又開始研究如何通過嚴格證明來驗證程序正確性,提出了一些方法。同時,機器證明的發展提供了使這種程序驗證過程自動化的可能性。近年來人們又發現,其他提高軟件可靠性的一些技術,如結構程序設計等,在和程序正確性證明結合起來使用時,會有更好的效果。這也推動了這方麵的研究。如從事高階軟件技術的研究的人曾指出,這一技術基本上是兩步。第一步是證明某些用高階語言寫成的子程序是正確的。第二步是使程序員能夠數學工作者在數學證明中用數學定理作組成部分那樣來使用這些子程序。將這些組成部分聯接起來就得到一個結構程序。
程序正確性證明目前還隻能用於較短的程序。在1974年夏用這種方法驗證過的最長的程序是一個編譯程序的一個子集合的編譯程序。