「串台」故障的原因终于揭晓；吴涛的莫尔斯码 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。这样，对于上述的一个代码片段 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 比测试更加完备和简洁。在实际工作中，我们往往会针对验证的程序的特点，设计特定的逻辑系统，以进一步的降低证明的难度和复杂度。
相关链接
- 读者 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 程序员，《内核恐慌》主播。