互动科普

11年前，美国新丹佛国际机场投入使用时，堪称建筑设计史上一大引人注目的奇迹。它那套全自动的行李处理系统，无疑是镶嵌在这座现代化机场上最为耀眼的高科技明珠。这套系统的传送带总长达26英里（约合42公里），可以保证所有行李经自动分拣后，迅速可靠地运送到飞机上或者乘客手中，各个环节的配合本应该准确无误、天衣无缝。然而这个系统从一开始就不断受到软件问题的困扰，以致机场的启用被耽搁了16个月之久，并为此多花费了数亿美元。经过数年的反复调试，这套系统始终毫无起色。去年夏天，机场管理层终于忍无可忍，决定让它彻底让位，重新启用传统的手工装卸行李车和有人驾驶拖车。设计这套机械化行李处理系统的BAE自动系统公司黯然停业，而该系统的主要用户——美国联合航空公司则跌入了破产的深渊。这套行李系统造成的混乱局面，无疑是两家公司败走麦城的重要原因之一。

蹩脚的软件设计使数百万用户吃尽了苦头，每天都付出沉重的代价。软件搞砸的事例不胜枚举，比较著名的有以下几个：1997年，美国税务总署（IRS）耗资40亿美元的升级计划惨遭失败，后来一项80亿美元的改造工程也同样遇到麻烦；2005年，美国联邦调查局（FBI）一套价值1.7亿美元的虚拟案件文档管理系统(virtual case-file management system)被迫报废；美国联邦航空管理局（FAA）试图改造日渐过时的空中交通管制系统(air-traffic control system)，但屡战屡败，至今仍无成功的迹象。

上述所有软件的悲剧都有一个共同点：当人们发现致命的设计失误时，为时已晚。软件设计人员都是着手编写代码（即计算机用来执行程序的指令）之后，才会发现软件的不足。有时，致命的矛盾或者冗长是故障的源头，但更常见的原因在于软件的总体设计含混、考虑不周，也就是决定软件功能以及如何组织成各个功能模块的基本构想存在着致命的矛盾。就像建造房屋一样，如果地基不稳，那么建造在地基上的软件也不会稳定。

在这些臭名昭著的软件设计败笔中，负有责任的主管们或许可以找借口来为自己开脱，说他们完全遵守了标准的行业惯例。不幸的是，他们这么说并没有错。软件开发人员几乎从来不会检验软件设计是否包含了要求的属性，进行足够的分析，这就是软件行业的惯例。但要记住，现在是电脑统治天下的时代，天上飞的飞机、地上跑的火车、汽车，全球众多金融、通信、销售和制造系统的运行，无不在计算机的操控之下。软件是否稳定关乎人命，关乎社会安全，因此我们迫切需要加强软件的稳定性。

现在有若干项针对软件设计的分析工具崭露头角(见74页的表格)。它们的原理和多年来工程师们用于检查计算机硬件的那些程序相仿。用高度概括、简洁的程序建立它的模型，然后利用该模型来试探软件系统各种可能的执行方案（或许多达数十亿种），在这一过程中查看是否会有导致软件失灵的意外状况出现。这样，软件设计人员就可以在软件用于某一具体场合之前发现错误。笔者所在研究小组开发的Alloy（可在网上免费下载），就是这类分析工具之中的一个实例。实践证明，它在诸如癌症治疗装置(见73页的表格)、加密系统以及航空用软件等各种迥然不同的应用场合中，都相当有效。

20多年以来，针对使用数学手段证明程序是否正确的方法，科学家进行了大量研究，Alloy及相关的一些软件设计检查工具，便建立在这些现有的研究成果基础之上。但这些工具并不需要人工完成证明，而是运用自动推理方法，把软件设计问题当作一个有待解决的复杂的智力游戏来处理。这些工具分析的对象是软件的设计，而不是程序的代码，因此它们不能担保程序不会崩溃。但是它们有望成为软件工程师手中第一批实用的分析工具，帮助工程师打造出坚强可靠、使用方便、易于开发的软件系统。

程序检验有新招

软件出故障并不是新话题。早在20世纪60年代初，就有人敲响了软件危机的警钟。只是在计算机广泛渗透到社会生活的方方面面之后，这个问题才越发严重起来[参见《科学美国人》1994年9月号W·韦特·吉布斯所著《软件的慢性危机》一文]。

现在大多数软件都通过测试来发现，并消除软件中存在的差错和漏洞。工程师们将多种不同的初始条件输入程序后，让程序运行，看看程序的工作状况是否与设计者的预期相吻合。虽然这种方法能查出一大堆小问题，却往往漏掉了软件基本设计中的缺陷。在某种意义上说，这些软件测试手段是捡了芝麻丢了西瓜：它们可以查出个别烂掉的树，却忽视了整片患病的森林。

更糟糕的是，在测试过程中被“纠正”过的差错，常常使软件的设计问题雪上加霜。在程序设计人员对代码进行查错调试，并加进新功能时，软件总是会变得更加复杂，这样，出现错误且效率下降的可能性也进一步增大。改写软件还会延长软件的开发时间，增加开发成本。对需要应付众多意外情况的大型软件系统（如空中交通管制程序）而言，这种局面格外让人厌烦。头痛医头、脚痛医脚的软件调试方法，使人回想起古希腊时代的行星运动理论——也就是已经被证明站不住脚的地心说。最初的地心说是由托勒密提出的，进入中世纪，越来越多的观测证据证明地心说并不准确，因此天文学家首次引入所谓的“本轮”对地心说进行修补，试图弥合理论与观测的矛盾。然而事实表明，加入这些本轮并没有解决问题，于是天文学家在本轮之上又加进新的本轮。几个世纪过去，不断进行的修补工作导致本轮越积越多。问题不仅没有解决，反而越发严重。小修小补难以奏效，因为根本观念从一开始就存在致命的缺陷。（本轮是人为规定的行星运行轨道，地心说认为行星绕着本轮旋转，本轮再沿着均轮围绕地球公转。到了中世纪后期，观察仪器不断改进，对行星位置和运动的测量越来越精确，观测数据与计算结果之间的偏差也越发凸现。人们曾用增加本轮的办法来补救，小本轮增加到80多个，仍不能精确地计算出行星的确切位置。）

无独有偶，容易出故障的软件跟地心说一样，多半都是越改越复杂，越复杂就越不可靠，无论花费多少时间和金钱进行修补都无济于事。众所周知，软件系统发生的严重问题很少是由编程错误造成的，几乎所有大麻烦，都可以追溯到编写程序之前所犯的基本观念错误上。在制定要求、规范或程序整体方案的最初阶段，只需少量的模拟和分析工作，就可以发现和纠正错误，花费仅仅相当于在后期对所有代码进行检查的费用的零头，而且效果并不比后者差多少。在整体设计阶段尽早察觉问题的苗头，可以避免后期出现代价昂贵的棘手故障。

软件设计工具的进展一直举步维艰，主要原因在于软件并不服从物理学法则。计算机程序实质上是由一个个二进制数字（比特）构成的数字对象，因此它们就像粒子那样是离散而非连续的。机械工程师在测试机械元件时，可以对元件施加一个很大的压力，如果元件能挺过来，就可以推断它在受到稍小的力的作用时不会失灵，因为这两种情况服从同一（连续性）物理法则。然而遗憾的是，这样的概括推理不适用于软件。我们不可能根据一个测试事例的结果来推断其他测试方案的情况。一段软件能正常工作，并不代表另一段类似软件也能正常工作，因为这两段软件是离散的、各自独立的。

在计算机理论发展初期，研究人员曾希望，程序设计者能像数学家证明定理一样证明自己编写的代码是正确的。然而这样的证明所涉及的众多步骤根本无法自动完成，因此大部分工作还是不得不由专家亲自动手。这种所谓“蛮干”的方法，总的说来是行不通的，一般只用在少数相对简单但极其重要的软件上（例如管理铁路交叉道口的软件）。

后来，研究人员开始采用另一种完全不同的方法——利用现今高速处理器强大的处理能力来测试每一种可能的情况。这种方法称为模型检查法，现已广泛用于验证集成电路的设计。它的基本构想是模拟实践中可能碰到的每一种状态序列（即软件在各特定时刻的状况），并确认任何一种状态序列均不会导致软件失灵。对微芯片设计而言，需要评估的状态数目常常大得难以想象：10100或者更大。而对软件而言，这个问题的严重程度并不亚于微芯片设计。不过我们可以把所有软件状态划分为一些庞大的集合，采用巧妙的编码方法非常紧凑地表示这些状态集，这样，只须同时考虑这些大集合，就能检查软件的每一种状态了。

遗憾的是，单靠模型检查不可能应付具有复杂结构的状态，而这类状态却正是绝大多数软件设计所共有的一个特征。我和我的同事们构想出一种新办法，基本思路不变，只是通过一种不同的机制来实现。同模型检查相仿，它也要考虑几乎所有可能的情况（不过，实际操作时需要设定若干界限，控制问题的规模，因为软件不会受硬件物理限制的约束），但与模型检查不同，我们的方法并不通过确定具体结果来直接检查，而是通过自动方式随机地、一次一位地逐步填满每一种状态，来搜索所谓“不良”状况，也就是可能导致软件失灵的情况。

在某种意义上，这一过程与机械手玩拼图的过程有异曲同工之妙：机械手随机把拼图游戏的各个图案一块块拼起来，直到完成。如果得出的拼图对应一种不良情况，那么Alloy的工作就算完成了。因此，Alloy实际上是把软件分析工作当作拼图游戏一样来处理。近来开发的其他某些软件模型检查工具的运作原理，也大同小异。

层层排除先简化

要想了解Alloy如何破解软件设计这样的拼图游戏，回忆一则古老的智力难题，或许会有所帮助。一位农夫到市场上买了一只狐狸、一只鹅和一袋玉米。回家路上，他必须带着他买的东西乘船渡过一条河。但是渡船很小，一次只能载一个人和一样东西过河。于是农夫面临着一个难题：如果他不在场管着，狐狸会把鹅吃掉，要不就是鹅把玉米吃掉。农夫怎样才能把他买的所有东西平安带到对岸呢？

这类智力游戏要求人们构想出满足一组约束条件的某种方案。我们可以纸上谈兵，通过想象一系列步骤来完成这一任务。农夫首先把鹅运到对岸，然后返回来把狐狸带走，从对岸折返时带上鹅，把鹅换成玉米带到对岸，最后再回来接鹅。考察一下每一步是否满足约束条件，我们就可确定农夫所买的东西最终都平安无事。

成功的软件设计也会提出类似的的一套规则，不过要复杂得多。检查设计的工具（如Alloy之类）要发挥作用，就必须具备发现反例的能力——所谓反例，就是指智力游戏的某些答案，满足所有约束条件（由此在程序运行过程中的确有可能出现），却得出一个不合要求的结果。只要有这类反例出现，那就说明程序的设计有问题。智力游戏玩家一旦找到“过河难题”的答案会高兴不已，但如果你发现软件设计这种拼图游戏有解，却是个坏消息，因为这意味着存在着不良情况，软件的设计有缺陷。在实践中，反例本身或许不会直接造成问题，它可能只是揭示了软件设计者当初在描述不合要求的结果时存在偏差。无论是哪种情况，反正都必须采取补救措施，要么修正软件设计，要么就修正设计者的期望。

搜索反例可能会遇到一个巨大的障碍：对于哪怕只有中等复杂的软件设计，约束条件、可以设想的情况这两者的数目，都将随着问题规模的扩大，以指数速度飙升。试想你在婚礼上负责安排谁跟谁坐在一起。如果所有来宾彼此相处都没有问题，当然不费吹灰之力。如果有几位来宾曾经是夫妻，为免尴尬需要分开坐，那就得费些功夫了。现在假定你要为罗密欧和朱丽叶的婚事安排来宾座位。如果有20个座位和10位来宾，而且每位来宾可以坐在任一座位上，那么座位安排方案总共有1020种可能。即使每秒可检查10亿种方案，一台计算机也要用三年时间才能完成。

不过，上个世纪80年代，研究人员发现了解决这类难题的捷径。这些难题被归类为所谓的“可满足度问题”（satisfiability problem）。其实，虽然这种问题中可能的情况不计其数，但我们可以将整批整批的情况排除掉——只要考察某一个部分解，并证明某一批人全部都肯定违反了某个相关的约束条件即可。随着电脑计算能力与日俱增，所谓的“SAT求解程序”（satisfiability solver，利用上述技巧来分析可满足度问题的程序）的效率有了突飞猛进的提高。现在许多SAT求解程序可免费得到，它们常常能解决有数百万个约束条件的可满足度问题。

抽象技巧显奇效

顾名思义，Alloy这个工具的作用，就是把提升软件品质的两大要素结合在一起。一个要素是一种新的语言，它有助于弄清软件设计的结构和各段功能代码之间的相互关系。另一个则是一种包含了SAT程序的自动化分析程序，它可以分析大量的可能状态。

应用Alloy的第一步是建立软件设计的模型。这种模型不是软件工程中常见的初步描述或流程图，而是详细说明系统及其各组成部分的“运动部件”和具体行为（包括需要的行为和不需要的行为）的精确模型。软件工程师首先写下软件设计中各类对象的定义，然后把这些对象归入不同的数学集合。也就是在结构和行为方面都相似（例如朱丽叶家族所有宾客的集合），并通过数学关系联系起来（例如把坐在一起的宾客联系起来）的一组事物。

然后我们来考虑制约这些集合和关系的事实。在软件设计中，事实包括软件系统的运作机制，以及与系统的其他组成部分有关的一些假定（比如用户可能会有什么样的行为）。有的事实只是简单的假设，比如说任何一位宾客不可能既是朱丽叶家族的人、又是罗密欧家族的人，每位宾客都正好挨着一左一右另外两位宾客等等。有的事实则与设计本身有关：例如，在我们的座位安排程序中，设计规则就是每一桌（除了首桌以外）要么分配给罗密欧家族的宾客，要么分给朱丽叶家族的宾客。

最后还有断言。所谓断言，就是可以从事实推导出的约束条件。在我们这个例子中，除了罗密欧和朱丽叶两人外，罗密欧家族的人不会与朱丽叶家族的人坐在一起，由此得出的断言是，系统永远不可能进入某些不合要求的状态，而特定的不良事件序列永远不可能出现。

Alloy工具的分析模块利用SAT求解程序来搜索反例。反例实质上就是软件系统的某些似乎合理的状态，软件的设计允许这种状态出现，但它们却无法通过合理性检验（进行合理性检验的方法，就是编写一些如果模型设计正确就一定为真的断言）。换言之，这个程序尝试构建出一些符合事实，但却同断言背道而驰的情况。在我们的例子中，它将得出一个不合要求的座位分配方案：在首桌，一位来自朱丽叶家族的人（不是朱丽叶本人）同一位来自罗密欧家族的人（也不是罗密欧本人）坐在了一起。为了修正这一座位安排规则，我们可以加进一个新的事实：罗密欧和朱丽叶两人独占首桌。这样，Alloy就找不到反例了。

上述集合、关系、事实、断言等等要素，一旦明确宣示后，合起来实质上就是对软件设计进行抓住核心的抽象化处理。详细写出这些抽象的对象之间的关系，就使软件设计的约束条件明朗化。更重要的是，它将促使软件工程师仔细思考究竟何种抽象具有最佳效果。许多软件系统要么是毫无必要地弄得非常复杂，要么是运行不可靠，究其根源，都是因为抽象方法选择不当之故。

如果系统依赖的软件以简单而可靠的抽象方法为基础，那么这样的系统将更方便。例如，电子售票系统大大简化了乘坐飞机的手续，通用产品条形码使购物更加方便舒适，而800会议电话促进了远程会议的实现。这些革新的问世，得益于我们改造了在基础软件中体现出来的根本抽象方法。

可靠软件一步遥

Alloy之类的工具目前主要用在研究及高科技行业中。不过，这项技术已用于探索电话交换系统的新型架构，设计可以抗御黑客的航空电子处理装置，并用来描述通信网的接入管理规则。我们已经运用此项技术检验了一些广泛使用的“强大”软件，例如搜索办公网络的打印机的协议，以及使多台机器上的文件同步的工具等。此外，Alloy还发现某些公开发布的软件包存在严重问题。例如，一项门钥管理协议，本应根据是否属于某团体来实施出入管理规则，但经过Alloy检验后，却发现它对于以前的成员也大开方便之门——这样的人本应该被拒之门外。值得一提的是，即使对那些用于最简单场合的软件设计，Alloy也发现它们的不少漏洞，问题之多，让用过Alloy的程序设计人员大吃一惊。

Alloy之类的检查工具广泛被业界采用，只是时间问题。作为基础的SAT求解程序不断获得改进，使这类分析工具的速度越来越快，处理大型系统的能力越来越强。与此同时，学过这些方法的新一代软件设计师，也将把它们运用到自己的工作中。模拟技术正迅速普及，特别在管理人员中更加深入人心。这些管理人员迫切希望，能看到除了程序以外对软件系统设计的描述。

到一定时候，软件可能成为整个社会日常基础资源中至关重要的一环，因此社会将再也不能容忍劣质软件。政府甚至可能制定相关的检查与许可条例，推行高质量的程序构建技术。有朝一日，通过精心的设计，软件系统可能将成为真正稳固、可预测并且便于使用的系统。