《内核恐慌》(Kernel Panic) 是吴涛和 Rio 做的播客,首播于 2014 年 10 月。号称硬核,可也没什么干货。想听的人听,不想听的人就别听。

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。这样,对于上述的一个代码片段 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 比测试更加完备和简洁。在实际工作中,我们往往会针对验证的程序的特点,设计特定的逻辑系统,以进一步的降低证明的难度和复杂度。

相关链接

人物简介