Yechiel Kimchi

半形式化地推理正確性#

試圖用手工對軟體正確性進行形式化證明，會產生比程式碼本身更長的證明，而且更可能包含錯誤。自動化工具較好但不一定總是可用。以下描述的是一條中間路線：半形式化地推理正確性（reasoning semiformally about correctness）。

核心方法#

基本方法是將所有待考慮的程式碼劃分為短的區段——從一行到一個函式呼叫，到不超過 10 行的區塊——然後論證它們的正確性。論證只需要強到能說服你的魔鬼代言人同儕程式設計師（devil’s advocate peer programmer）。

區段端點的狀態#

每個區段的選擇應使得在端點處，程式的狀態（state of the program）（即程式計數器和所有「活著的」物件的值）滿足一個容易描述的屬性，並且該區段的功能容易描述為單一任務。這些端點屬性可推廣為：

• 前置條件（preconditions）和後置條件（postconditions）——用於函式
• 不變量（invariants）——用於迴圈和類別

實用的編碼準則#

許多編碼實踐雖然廣為人知（但可能執行得不夠好），被認為是「好的」，都能讓推理變得更容易。光是打算推理你的程式碼，你就已經開始朝著更好的風格和結構邁進了：

• 避免使用 goto 語句，因為它們使遠端區段高度相互依賴
• 避免使用可修改的全域變數（global variables），因為它們使所有使用它們的區段相互依賴
• 每個變數應有盡可能小的作用域（scope），例如區域物件可以在第一次使用前才宣告
• 盡可能讓物件不可變（immutable）
• 用間距使程式碼可讀——水平和垂直都是——例如對齊相關結構、用空行分隔兩個區段
• 透過選擇描述性（但相對簡短）的名稱來讓程式碼自我文件化（self-documenting）
• 如果需要巢狀區段，將其提取為函式
• 讓函式簡短且專注於單一任務。舊的 24 行限制仍然適用——雖然螢幕尺寸和解析度改變了，但人類認知從 1960 年代至今沒有改變
• 函式應有少量參數（四個是不錯的上限）。將相關參數分組到單一物件中，可以將**物件不變量（object invariants）**局部化，簡化推理
• 每個程式碼單元，從一個區塊到一個函式庫，都應該有窄介面（narrow interface）。較少的溝通意味著較少的推理負擔

回傳內部狀態的 getters 是一種負擔——不要向物件索取資訊來做事，而是要求物件用它已有的資訊來做事。換句話說，封裝就是——而且僅僅是——關於窄介面（encapsulation is all—and only—about narrow interfaces）。

避免使用 Setters#

為了保持類別的不變量，應該避免使用 setters。Setters 容易讓物件的狀態被打破。

推理帶來的額外收益#

除了推理正確性之外，對程式碼進行論證還能幫助你更好地理解它。將你的洞見傳達出來，對所有人都有益處。