ch4. 結構化程式設計
Edsger Wybe Dijkstra 於 1930 年出生在鹿特丹。他在第二次世界大戰期間倖存於鹿特丹的轟炸，以及德國對荷蘭的占領，並於1948年以數學、物理、化學、生物最高分從高中畢業。1952年3月，21歲的 Dijkstra 在阿姆斯特丹的數學中心找到工作，成為荷蘭第一位程式設計師。
1955年，已經當了三年的程式設計師，且同時身為學生的 Dijkstra 得出一個結論：程式設計的智力挑戰比起理論物理學還大。因此，他選擇了程式設計作為他的長期職業。
1957年，Dijkstra 與 Maria Debets 結婚。當時，在荷蘭結婚必須登記職業，荷蘭的公家機關並不接受 programmer 這個職業，他們從未聽過這樣的職業，為了滿足他們，Dijkstra 在職業欄中將自己定位為「理論物理學家」。
Dijkstra 與他的老闆 Adriaan van Wijngaarden 討論著以程式設計當作他的生涯志向，他認為沒有人會將程式設計視為一門學科或是科學，因此他認為自己可能不會被認真以待，然而他的老闆回答說，Dijkstra 將有可能成為那位發現新學科，以致於將軟體變成一門科學的人。
Dijkstra 在真空管時代開始了他的職業生涯，當時的計算機很巨大、脆弱、緩慢、不可靠、且極其有限。在早期，程式是二進制或是非常粗糙的組合語言編寫的，並以紙帶或打孔卡片作為輸入的這種物理形式存在，編輯/編譯/測試的循環就需要數小時甚至數天的時間。
正是在這個原始的環境造就了 Dijkstra 做出了他偉的的發現。
證明
Dijkstra 很早就發現，程式設計是一件難事，且程式設計師也不容易將它做好。任何複雜的程式都包含了太多人類大腦在沒有幫助下可以管理的細節。忽視一個極小的細節程式看似可以運作正常，但卻可以以出人意料的方式失敗。
Dijkstra 的解決方案是應用數學的證明法。他的願景是建立一個如同歐基里得的公理、定理、推論和引理的層次結構。Dijkstra 認為程式設計師可以像數學家一樣使用這樣的證明方法，換句話說，程式設計師應該要運用這些經過驗證的結構，並將它們與自己證明正確的程式碼相結合。
當然，為了使這一切開始進行，Dijkstra 意識到他必須要撰寫一些範例以展示如何用基本的證明方法來證明簡單的演算法，而他發現這是一件極具挑戰性的事。
在調查的過程中，Dijkstra 發現某些使用 goto 語句的情況會阻止模塊被遞迴地分解成更小的單元，從而阻礙了使用分而治之的方法進行證明的可能性。
然而，goto 的其他用途卻沒有這個問題。Dijkstra 意識到，「好的」goto 使用方法對應到簡單的選擇和迭代控制結構，例如 if/then/else 和 do/while。只使用這些控制結構的模塊才可以被遞迴的切割成可以被證明的單元。
Dijkstra 認識到，當這些控制結構與順序執行相結合是特殊的。在當時的兩年前，已經由 Böhm 和 Jacopini 證明了，所有程式都可以由三個結構建構而成：順序(sequence)、選擇(selection)、迭代(iteration)。
這個發現非常了不起：使一個模塊可證明的控制結構，正是構成所有程式的最小控制結構集合。因此，結構化程式設計應運而生。
Dijkstra 證明了順序語句可以通過簡單的列舉來證明其正確性。這種技術利用數學方法系統性地追蹤語句的輸入與輸出，與一般的數學證明無異。
Dijkstra 通過重新應用列舉法來解決選擇問題，對於選擇中的每條路徑都進行了列舉，如果所有的路徑都產生了適當的數學結果，那麼就表示證明是可靠的。
迭代則有些不同，為了證明迭代的正確性，Dijkstra 必須使用歸納法。他通過列舉證明了 1 得情況，然後他再次通過列舉證明了如果假設 N 是正確的，則 N+1 也是正確的，他也證明了迭代的起始條件與結束條件的正確性。
這樣的證明是費時且複雜的，但它們具備了證明的意義。隨著它們的發展，建立一個歐基里得式階層式的定理看似變得可行。
一個有害的聲明
1968年，Dijkstra 給 CACM 的編輯寫了一封信，該信在三月份的期刊上發表。這封信的標題是「Go To Statement Considered Harmful」。該文章概述了他對三種控制結構的立場。
而程設界也因此掀起了一場熱潮。當時我們還沒有網路，所以人們無法在網上對 Dijkstra 進行網路攻擊，但他們可以向許多發行的期刊投信。
這些信件不一定都很客氣，有些甚至十分負面，而有些則表達了對他的支持，於是兩方的戰爭開始，並持續了約十年。
最終爭論逐漸消失了。原因很簡單：Dijkstra 獲得了勝利。隨著電腦語言的演進，goto 語句逐漸被淘汰，幾乎消失殆盡。大多數現代語言都不再使用 goto 語句，在 LISP 這個程式語言中，甚至從來就沒有使用過。
現在我們都是結構化程式設計師，雖然不一定是出於選擇。只是因為我們的語言不給我們使用無紀律的直接控制轉移的選擇。
有些人可能會指出 Java 中的命名中斷或異常作為 goto 的類比。事實上，這些結構並不像 Fortran 或 COBOL 等舊語言一樣完全無限制地轉移控制。實際上，即使是還支持 goto 關鍵字的語言，也常常將目標限制在當前函數的範圍內。
函式分解
結構化程式設計允許將模塊遞歸地分解為可證明的單元，這意味著模塊可以被功能性地分解。也就是說，您可以將一個大規模的問題陳述分解為高層次的函數。然後，每個函數可以進一步分解為低層次的函數，無窮無盡。此外，每個分解的函數都可以使用受限的控制結構來表示。
在此基礎上，結構化分析和結構化設計等學科在 1970 年代末至 1980 年代間變得流行起來。像是 Ed Yourdon, Larry Constantine, Tom DeMarco 和 Meilir Page-Jones 這樣的人在那個時期推廣和普及了這些技術。通過遵循這些學科，程序員可以將大型的預計系統分解為模塊和組件，進一步將其細分為可證明的小型功能。
不再使用正式證明
我們沒有等到一個系統且完整的證明出現，歐幾里得式的層狀結構理論從未被建立，廣大的程式設計師從未看到耗費大量力氣證明每個小函式正確性所帶來的好處。最終，Dijkstra 的夢想逐漸消失。人們很少有人相信透過嚴謹的證明才能產生高質量的軟體。
當然，正式的、歐幾里得風格的數學證明並不是證明某事正確的唯一策略。另一種極為成功的策略是科學方法。
科學拯救大業
科學與數學在根本上有所不同，那就是科學理論和定律無法被證明為正確。我無法向你證明牛頓的第二運動定律，\(F = ma\)，或是萬有引力定律，\(F = Gm_1m_2/r^2\)是正確的。我可以向你展示這些定律，並且我可以進行測量來證明它們在許多小數點後都是正確的，但我無法以數學證明的方式來證明它們。無論我進行多少實驗或收集多少實證，總是有可能某個實驗會顯示那些運動和引力的定律是不正確的。
這就是科學理論和定律的本質：它們是可證伪的，但不可證明的。
然而，我們每天都憑藉這些法律來賭上我們的生命。每次你上車的時候，你肯定相信 \(F = ma\) 是對世界運作方式的可靠描述。每當你踏出一步，你就賭上你的健康和安全，相信 \(F = Gm_1m_2/r^2\) 是正確的。
科學的運作方式並非通過證明陳述為真，而是通過證明陳述為假。那些我們無法證明為假的陳述，在經過大量努力後，我們認為它們對我們的目的來說足夠真實。
當然，並非所有陳述都是可證明的。陳述「這是謊言」既不是真的也不是假的。這是一個最簡單的不可證明陳述的例子之一。
最終，我們可以說數學是證明可證明的陳述為真的學科。相反，科學是證明可證明的陳述為假的學科。
測試
Dijkstra 曾說過：「測試只能顯示會誤的存在，而不能證明其不存在。」換句話說，一個程式可以通過測試被證明是錯誤的，但無法被證明是正確的。在充分的測試過後，測試只能讓我們認為一個程式對我們的目的來說是否足夠正確。
這個事實的含義令人驚嘆。軟體開發並不是一個數學的努力，儘管它似乎在操作數學結構。相反，軟體就像一門科學。我們通過無法證明錯誤來展示正確性，儘管我們盡了最大的努力。
這樣的錯誤證明只適用於可證明的程式。一個無法證明的程式，例如由於無節制地使用goto，無論進行多少次測試，都無法被視為正確。
結構化程式設計迫使我們將程式遞歸地分解為一組小的可證明函數。然後，我們可以使用測試來嘗試證明這些小的可證明函數的不正確性。如果這些測試無法證明不正確性，那麼我們認為這些函數對於我們的目的來說足夠正確。
結論
正是這種能力創造了可驗證的程式設計單元，使得結構化程式設計在今天仍然具有價值。這也是現代語言通常不支援無限制的goto語句的原因。此外，在架構層面上，這也是為什麼我們仍然認為函式分解是我們的最佳實踐之一。
從最小的功能到最大的組件，軟體在各個層面上都像是一門科學，因此受到可證伪性的驅動。軟體架構師致力於定義易於證伪（可測試）的模塊、組件和服務。為此，他們運用類似結 構化程式設計的嚴格紀律，只是在更高的層次上。
在接下來的章節中，我們將詳細研究這些限制性的學科。