赵翔鹏的Blog Xiangpeng's Thinkpad

Bill Gates与Joel Spolsky对形式化方法的评价

Billg对formal methods的评价是我第一次看到。跟Joel Spolsky的评价对比一下，很有趣。

1、Microsoft 的 SDV 经验：通过静态验证提高 Windows Vista 驱动程序的质量

Static Driver Verifier (SDV) 是一种基于规则的编译时静态分析工具，用于验证用 C 代码编写的 Windows 驱动程序。SDV 根据使用 Windows 设备驱动程序接口的精确规则集对驱动程序进行验证，然后报告这些规则的任何违规行为。

Microsoft Research (MSR) Software Productivity Tools 小组投入了多年的工作来创建一种引擎，以便自动检查基于 C 的程序是否正确使用与外部库相连的接口。此项目在 MSR 中称为 SLAM，最终的成果是一个已经集成到 SDV 的强大分析引擎。

以下引用了 Microsoft Research 小组的话，来自 MSR 网站上的“提供用于技术转移的模板”：

• 选择问题。“我们选择了一个重要但并非不能克服的问题领域进行研究（设备驱动程序）。……我们有机会了解 Windows 源代码和设备驱动程序源代码。此外，我们还能够广泛接触设备驱动程序和 Windows 领域的一流专家”。

• 站在巨人的肩膀上。“SLAM 拥有几十年使用正式方法和编程语言进行研究的经验。我们非常庆幸，在 Microsoft Research、Windows Division 以及 Microsoft 之外有许多人为 SLAM 和 SDV 出策出力”。

• 研究环境。“Microsoft 的产业研究环境以及普遍的动手/实干氛围使我们能够放手尝试使用危险的解决方案来解决重大问题，还可以提供我们迫切需要的支持。”

• 软件工程。“我们采用‘开放式’的体系结构风格来开发 SLAM，对每个核心组件使用非常简单的概念接口。这使我们能够迅速使用各种工具进行试验，设定一套我们认为最能解决问题的算法。这种体系结构使我们很容易对各种组件进行重新配置以对新问题做出反应。”

• 在工作中使用正确的工具。“我们使用法国研究机构 INRIA 的 Objective Caml 函数编程语言开发 SLAM。该语言的表达力及其实现的稳定性极大地提高了生产效率。”

SDV 目前在 Microsoft 内部使用，在 WDK 的测试版本中也提供了这种工具。它的宗旨在于使 Microsoft 及其合作伙伴能够提供高质量的设备驱动程序。

比尔盖茨在 OOPSLA 2002 上的发言：

为了进行丰富的静态分析，我们已经开发了许多东西。实际上，我们花了 3000 多万美元请其他公司开发此类工具，现在我想说的是，希望您们将精力集中在将这些工具应用于大规模软件系统上，在 Windows 或 Office 的源代码中都包含此种系统，看看到我们到底能取得什么样的进展。

让我们回顾一下，就证实程序是否以特定方式运行的能力来说，有哪些尖端技术？几十年来，这种问题一直存在。当我从哈佛退学时，这曾是一个让我感兴趣并努力解决的问题，实际上当时我还在想，如果我去开一家公司，情况可能会十分糟糕，我会错过在软件程序检验方面的一些重大突破，因为我需要忙于处理员工的工资单。事实证明，看来我还并未错过太多（笑着说道），我想说的是，在某种程度上，这已经是一个非常紧迫的问题。虽然不可能实现一种完全通用的解决方案，但是对于许多非常有趣的特性，这种检验的思想已经成为可以帮助我们的长效方法，仅在去年这一点已经得到充分的体现。

我们称执行这种检验的系统为模型检查系统。您需要定义约束，包括很简单的事情：已经获取锁的人不得再次获取；没有获取锁的人不得释放锁；以及您想要确定其运行良好的代码多线程方面的内容。在本例中，您使用 C 代码本身去描述这些，然后分析程序会仔细检查并缩减程序，去掉不影响其路径分析的任何内容，进行路径分析来确定整个程序中是否有路径违反约束。

我们首次应用此解决方案的领域是设备驱动程序。

第 17 届年度 ACM 讨论会 - 面向对象的编程、系统、语言和应用程序

2、《软件随想录》：Joel Spolsky对计算机学生的七大建议

我依然清楚记得我发誓绝不读研究生的那一刻。那是在一门叫做“动态逻辑”的课程上，教师是活力十足的耶鲁大学教授Lenore Zuck，她是计算机系那些聪明的老师中最聪明的人之一。

如今， 由于记忆力糟糕， 我已经差不多把这门课的内容忘光了，但是不管怎么说，在这里我还是想要对付着说一下。大致上，形式逻辑的意思是说，如果条件成立，你就能证明结论也成立。比如，根据形式逻辑，已知“只要成绩好，就能被雇用”，然后假定“Johnny的成绩好”，你就可以得到一个崭新的结论“Johnny会被雇用”。这完全是经典方法。但是，一个解构主义者（deconstructionist）只需要10秒钟就能破坏形式逻辑中所有有用的东西。这样一来，留给你的只是一些趣味性，而不是实用性。

现在再来说动态逻辑。它与形式逻辑其实是一回事，但是必须再多考虑时间因素。比如，“你打开灯之后，就能看见自己的鞋子”，已知“灯以前是亮的”，那么这就意味着“你看见了自己的鞋子”。

对于像Zuck教授那样聪明的理论家，动态逻辑充满了吸引力，因为它看上去很有希望让你在形式上证明一些计算机程序的相关理论问题。这样做说不定很有用。比如，你可以用它在形式上证明，火星漫游车的闪存卡不会发生溢出（overflow）问题，不会因而整天一遍又一遍地重启，耽误了它在那颗赤红色的星球上漫游寻找火星人马文（Marvin the Martian）。

在第一堂课上，Zuck博士写满了整整两面黑板，甚至黑板旁边的墙上都写上了很多证明步骤。需要证明的问题是，有一个控制灯泡的开关，现在灯泡没有亮，这时你打开了开关，请证明灯泡将会点亮。

整个证明过程复杂得不可思议，处处都是陷阱，必须十分小心。保证这个证明不出错太困难了，还不如直接相信打开开关灯就会亮。真的，虽然证明过程写满了许多块黑板，但是还是有许多中间步骤被省略了，因为如果要从形式逻辑上完整证明所有步骤，那就琐碎得无法形容了。许多步骤是用各种经典的逻辑证明方法推导得到的，包括归纳法、反证法等，甚至有些部分还是由旁听的研究生证明的。

留给我们的课后作业是证明逆命题：如果灯原来是关着的，现在却亮了，那么请证明开关的状态一定同原来相反。

我动手开始证明，我真的去证明了。

我在图书馆里待了很长时间。

我对照着Zuck博士的原始证明想依样画葫芦。研究了几个小时之后，我在其中发现了一个错误。可能我抄写的时候抄错了，但是这使得我想通了一件事。如果花费3个小时，写满了一块又一块的黑板，每一秒钟都可能出错，最后能够证明的却只是一个很琐碎的结论，那么这种方式有多大的实用性呢？在活生生、充满趣味的现实世界中，你永远都不会有机会使用它。

但是，动态逻辑的理论家们对这一点不感兴趣。他们看上它不是因为它有用，而是因为它可以为他们带来终身教职。

我放弃了这门课，并且发誓绝不会去读计算机科学的研究生。

这个故事告诉我们，计算机科学与软件开发不是一回事。如果你真的非常幸运，你的学校可能会开设很像样的软件开发课程。但是另一种可能是，你的学校根本不教你在现实中如何编程，因为精英学校都觉得，教授工作技能最好留给职业技术学校、犯人重返社会的培训项目去做。你到处都能学怎么写代码。别忘了，我们是耶鲁大学，我们的使命是培养未来的世界领袖。你交了16万美元的学费，却在学循环语句的写法，这怎么可以？你以为这是什么地方，难道是机场沿途的酒店里临时拼凑起来不靠谱的Java语言培训班？哼哼。

麻烦在于我们没有一种真正教授软件开发的专门学校。你如果想成为一个程序员，你可能只能选择计算机科学专业。这是一个不错的专业，但是它同软件开发不是一回事。在那些400等级的课程代号中，去寻找名称中带有“Practicum”这个词的课程吧（编者注：指供人实习的课程）。不要被这个拉丁语单词吓倒，这些都是有用的课程，之所以起这种名字，只是为了让那些文绉绉、装腔作势、满嘴胡说八道的公司经理们觉得高深莫测。