「串臺」故障的原因終于揭曉；吳濤的莫爾斯碼 app 主意看來目前不可行；三封很長的讀者反饋；主題是設計模式。兩位主持人不約而同地病了，所以沒有講新聞。 節(jié)目中提及的讀者 Haozhong Zhang 來信節(jié)選： 相對的，在 Formal Verification 中，舉個例子，我們可以把每條指令的執(zhí)行形式化表示成 {P}C{Q}，其中 C 是這條指令，P 稱為前條件 (Pre-condition) 描述了 C 執(zhí)行之前機器的狀態(tài) (例如某個寄存器的值是什么，某個內(nèi)存單元的值是什么，通常不需要覆蓋所有的寄存器和內(nèi)存單元，僅需要根據(jù)驗證的 Specification 選取我們關心的部分), Q 稱為后條件 (Post-condition) 描述了 C 執(zhí)行后的機器狀態(tài)。注意，這里 Q 同時描述 C 被中斷和不被中斷的執(zhí)行后的機器狀態(tài)。非形式化的，{P}C{Q} 表示在滿足前條件 P 的機器上執(zhí)行指令 C 得到的機器狀態(tài)滿足后條件 Q。這樣，對于上述的一個代碼片段 C1; C2; …; CN 我們有 {P1}C1{Q1}，{P2}C2{Q2}, …, {PN}CN{QN}。然后，我們證明 Q1 ? P2, …, QN-1 ? PN， 從而可以證明 {P1}C1; C2; …; CN{QN}。 同樣的，如果這個代碼片段的 Specification 也可以寫成，例如， {P}C1; C2; …; CN{Q}， 我們只需要再證明 P ? P1 和 QN ? Q， 即可以證明這個代碼片段的確滿足了給定的 Specification。因為這里的 P，Q，Pi, Qi 等描述了所有的可能情況，并且只需描述 Specification 關心的部分，所以這里的 Formal Verification 比測試更加完備和簡潔。在實際工作中，我們往往會針對驗證的程序的特點，設計特定的邏輯系統(tǒng)，以進一步的降低證明的難度和復雜度。 《內(nèi)核恐慌》網(wǎng)站：http://kernelpanic.fm ，捐款地址：http://kernelpanic.fm/donate