20. 设计模式

「串台」故障的原因终于揭晓；吴涛的莫尔斯码 app 主意看来目前不可行；三封很长的读者反馈；主题是设计模式。两位主持人不约而同地病了，所以没有讲新闻。

节目中提及的读者 Haozhong Zhang 来信节选：

相对的，在 Formal Verification 中，举个例子，我们可以把每条指令的执行形式化表示成 {P}C{Q}，其中 C 是这条指令，P 称为前条件 (Pre-condition) 描述了 C 执行之前机器的状态 (例如某个寄存器的值是什么，某个内存单元的值是什么，通常不需要覆盖所有的寄存器和内存单元，仅需要根据验证的 Specification 选取我们关心的部分), Q 称为后条件 (Post-condition) 描述了 C 执行后的机器状态。注意，这里 Q 同时描述 C 被中断和不被中断的执行后的机器状态。非形式化的，{P}C{Q} 表示在满足前条件 P 的机器上执行指令 C 得到的机器状态满足后条件 Q。这样，对于上述的一个代码片段 C₁; C₂; …; C_N 我们有 {P₁}C₁{Q₁}，{P₂}C₂{Q₂}, …, {P_N}C_N{Q_N}。然后，我们证明 Q₁ ⇒ P₂, …, Q_N-1 ⇒ P_N， 从而可以证明 {P₁}C₁; C₂; …; C_N{Q_N}。 同样的，如果这个代码片段的 Specification 也可以写成，例如， {P}C₁; C₂; …; C_N{Q}， 我们只需要再证明 P ⇒ P₁ 和 Q_N ⇒ Q， 即可以证明这个代码片段的确满足了给定的 Specification。因为这里的 P，Q，P_i, Q_i 等描述了所有的可能情况，并且只需描述 Specification 关心的部分，所以这里的 Formal Verification 比测试更加完备和简洁。在实际工作中，我们往往会针对验证的程序的特点，设计特定的逻辑系统，以进一步的降低证明的难度和复杂度。

相关链接

• 读者 Wang Jian 发来的 TDD 实践视频：YouTube、优酷
• Design Patterns: Elements of Reusable Object-Oriented Software
• 艾舍尔《天鹅》
• Erich Gamma
• Design Patterns 15 Years Later: An Interview with Erich Gamma, Richard Helm, and Ralph Johnson
• Hacker’s Delight
• 《编程珠玑》
• 《建筑的永恒之道》
• Cocoa Design Patterns
• C# Delegate/Event
• Patrick Naughton
• Python Pattern: “Borg”
• God Object
• Golden Hammer
• The Lone Ranger

人物简介

• Rio：《IT 公论》主播，IPN 联合创始人，Apple4us 程序员。
  
• 吴涛：Type is Beautiful 程序员，《内核恐慌》主播。