整潔架構 - ch4 結構化程式設計

這邊的主角是上一章節提到的 Edsger Wybe Dijkstra。

Dijkstra 於 1968 年發表的結構化程式設計，他證明了使用無限制地跳耀(goto 語句)對於程式的結構是有害的。比起這樣的跳耀他更推薦使用 if/then/else 和 do/while/until 來建構程式。

(第一段主要是在講歷史小故事，有興趣的人可以自己看一下)

證明

Dijkstra 認為程式設計師可以像數學家一樣，使用數學證明的層次結構來證明程式是正確的

Dijkstra 想要使用真正數學意義上的證明(proof)，他想建立一個歐幾里德式的數學證明層次，亦即公設(postulate)、定理(theorem)、引申定理(corollary)和輔助定理(lemma)

但他失敗了

原因是因為他發現在使模組遞回的被分解成越來越小的單元時， goto 語句 的某些使用方式會使分解過程失敗，而無法被分解為粒度夠小的單元的前提下，就會讓他無法去證明。

（在理解了 goto 語句及用法後好像會發現，這種失敗感覺起來可能跟深度的強依賴有關聯）

而在這樣試圖證明的過程中，Dijkstra 發現某些 goto 語句的用法並不會導致證明失敗，例如：if/then/else 和 do/while/until 。
模組若只使用這類型的控制結構，就有辦法分解為可證明的單元。

Dijkstra 發現只又是由以下三種結構組合而成的結構，都可以被分解成可證明的最小單元，三種結構分別是

這三種結構是由 Böhm 及 Jacopini 提出 (Structured program theorem)

每一種都有各自的證明方法及思考方向，但這邊先不贅述。

$$
S = { sequence, selection, iteration } \
\mathcal{P}(S) = 可建構所有程式的控制結構
$$

Dijkstra 立馬昭告天下想告訴世人「goto 語句是有害的」，結果自然是引發了一場宗教戰爭，直到隨著電腦語言的發展， goto 語句被淘汰。

總而言之，結構化程式設計允許將模組遞回的分解成可證明的單元。

但是證明從來沒有完成過，確切點應該是說，如同歐幾里德式數學證明層次般的正式證明從來沒有完成過。

書上提到，歐幾里德式數學證明層次般的證明並不是證明事情正確的唯一策略，另一個成功的策略是科學方法。

這邊的敘述筆者是有異議的，科學上的證明通常是建立於可模擬的情況下的實驗推導出的結果，但並非所有的事情都可以將所有的狀況模擬，這也是為什麼在科學的領域關於我們認定對的事情會使用定律 (theory) 而非定理 (theorem)，「正確」及「足夠正確」是不同的。

這段有提到關於科學上的證明，並非是要證明陳述是正確的，而是要證明陳述是錯誤的。而我們經過足夠多的努力仍然不能夠證明論述是錯誤的話，那麼就表示論述越接近真實。

Dijkstra 曾經說過：「測試顯示了錯誤的存在，而不是沒有錯誤」。承上一段，一個程式可以用測試來證明他是不正確的，但不能因此證明他是正確的，而經過足夠多的測試去驗證錯誤之後，我們可以得到「足夠」正確的程式。

軟體開發並不是試圖以數學來實現某個目標，儘管他操作的方式似乎是數學結構。

在提及了結構化程式設計的歷史淵源後，關於這個範式重要的原因是，「功能分解」在架構的層面上是一種非常實用的實戰技巧。