这个标题当然很有挑衅的味道。我们都会认为，这一宣言是针对着某些不可能的事情。不可能！环视四周，我们还做不出无缺陷的系统。如果这件事有可能，应该早就被人们做好了。再说，无论如何，我们首先要说清楚什么是“缺陷”。
我们该怎么想象这里的情况呢？我们可能想，这应该是一位大师想兜售他最新的灵丹妙药。亲爱的读者，请放心，这个序言并不包含任何全新的克敌法宝，而且进一步说，它也不是技术性的，不要求你理解一大堆复杂的概念。本序言的意图，就是提醒你注意一些简单的事实和想法。如果愿意，你就可以去利用它们。这里的思路就是去扮演某个人的角色，这个人现在正面临一种险恶的局面（是的，计算机化的系统的开发并没有远离险境—作为一种度量的尺度，只需要考虑在系统崩溃时所浪费的金钱）。在面临险境时，我们有可能决定以某种鲁莽的方式去改变某些东西。但是，这样做通常完全无效。另一条途径就是逐步引入一些简单的特征，希望把它们放在一起，最终能导致局面的全局性改变。后者也就是我们将要用在这里的“哲学”。
定义和需求文档
我们的目标就是构造出正确的系统，因此，首先需要认真地定义一种方法，据此可以判断自己做出的东西究竟是什么。这就是“定义和需求”文档的用途。在投身于开发一个计算机化的系统之前，必须认真地写出这种文档。
但是，你会说，大量工业部门都有这种文档，它们已然存在，为什么还要为此操心呢？好吧，就我个人的经验，绝大多数情况是，业界正在使用的文档非常糟糕。仅仅是理解需求到底是什么，将其从有关文档中提取出来，通常就已经很困难了。一个事实是，人们常以做文档时用了某些（昂贵）工具的事实作为其需求文档值得信任的证据！
我强烈建议，应该按照本节中说明的简单路线重写需求文档。
这样的一个文档应该包含两类相互嵌套的正文：解释性的正文和参考性的正文。前者包含为理解手头问题所需要的解释，当读者第一次遇到这里的问题，或者需要某些基本的理由时，这些解释应该能帮助他们。后者包含定义和需求，其形式主要是带有标签和编号、用自然语言写出的简短陈述句。与相应的解释相比，这种定义或需求应该更形式化。当然，它们必须是自足的，而且能成为判断正确性的唯一参考。
定义和需求文档应该类似于数学书籍，其中一段段的解释性文字（在这里，作者非形式化地解释自己的方法，有时还给出一些历史背景）里交织着一些更形式化的片段—定义、引理和定理—所有这些构成了参考性正文，很容易与书中的其他内容区别开来。对于系统工程的情况，我们用两个坐标来标记参考性的定义和需求。第一个坐标说明其用途（功能、设备、安全性、物理单元、退化模式、错误等），第二个坐标说明其抽象层次（高层、中间层、底层等）。
我们必须仔细地定义好第一个坐标，然后再去写定义和需求文档，因为对于不同的项目，这个坐标的情况有可能不同。注意，“功能性”标签描述目标软件中处理特定任务的需求，而“设备”标签描述环境必须保证的假设（我们也称其为需求）。我们的目标软件将运行于这种环境中。这种环境由一些设备组成，还包括一些物理变化现象、其他的软件部分，以及系统的用户。第二个坐标把参考性的项目放到一个层次结构中，从非常一般（抽象）的定义或需求，直到越来越特殊的、为了系统的运行而需要的东西。
这其中有一件事非常重要：在这个工作阶段，有关的定义和需求文档都必须得到利益相关方的同意和认定（签字）。
到了这个阶段的最后，我们已经写下有关目标系统的所需性质。这些东西到底能不能实现，我们还没有任何保证。即使我们写下所需要的飞机必须能飞，也不保证它真能飞起来。在写出了这样的文档后，人们经常会急于去编程。而我们都知道这样做将会得到什么。在投入编程之前，还需要有一个中间工作阶段，其作用将在下一节解释。
模拟和编程
程序设计活动的目标是构造出一段形式化正文。我们假定这段正文能指导计算机，告诉它怎样去完成一些特定的任务。我们的想法是不做这件事，而是去构造一个系统，其中有一部分是软件（也是我们将构造出的东西），它是系统许多部分中的一个。这也就是我们不把自己的工作仅限于去开发软件部分的原因。
为了像工程师一样做好这件事。我们并不假定是要指导计算机，而是假定要指导自己。要以严格的方式完成这件事。我们没有别的办法，只能是设法去做出未来系统的一个完全的模型，包括最后将要构造出的那个软件以及它的环境。该环境（同样）由一些设备、变化的物理现象、其他软件以及可能的用户构成。程序设计语言无助于我们完成这些工作。
所有这些都必须认真地建模，并设法弄清软件将如何运行的所有假设。模拟是系统工程师最主要的工作。程序设计则将随之变成了一种从属性的工作，它完全可以全自动地完成。
建模一个计算机化的系统，过去是借助于某种建模语言—例如 SIMULA-67（它是所有面向对象语言的鼻祖）—完成的，现在仍然如此。我们对此的建议仍然是做一个模拟，但不是用某种模拟语言来做这件事。为了便于检查和分析这一工作的结果，我们建议用构造数学模型的方式来完成它，通过证明来分析得到的模型。物理学家或者运筹学家就是这样工作的，我们也应该采用类似的做法。
因为我们并不打算指导计算机，所以不必去说需要一步步地做什么。我们要做的是解释并形式化地描述应该观察到的情况。但是，要这样做时，立刻就会遇到一个问题：我们如何才能去观察某种当时并不存在的东西？对这个问题的回答很简单：虽然它还没有存在于物理世界中，但显然它已经存在于我们的脑海里。工程师或建筑师总是这样做的：他们根据自己脑海中已有定义的某种表示，去构造出相应的实际物品。
离散迁移系统和证明
正如前一节所言，建模工作并不仅仅是形式化未来系统在我们脑海里的表示，还包括证 明这一表示能满足某些期望的性质等相关工作，也就是在前面讨论定义和需求文档时，非形式化地说明了的那些性质。
为了完成这一包含了模拟和证明的工作，我们采用一种简单的形式化工具，称为离散迁移系统。换句话说，无论需要执行的模拟工作是什么，我们总是把未来系统的组件表示为一些状态的序列。状态之间是突然出现的迁移，也称为事件。
从模拟的观点看，理解下面的情况非常重要：一个人按动一个按钮，或者一个发动机的启动或停止，或者一部分软件执行某项任务，如果这些都出现在某个全局性的系统里，那么它们之间并没有任何本质性的差异。这些活动中的每一个都是离散迁移系统，它们自行工作或相互通信，都在参与作为一个整体的某个系统的分布式活动。这些也就是我们计划采用的建模各种任务的方法。
使用这一非常简单的工作方式也极其方便。特别是有关的证明工作，其中一部分工作就是证明每个组件的迁移都能维持一些全局性质，而这些性质是我们所希望的，组件的所有状态都必须始终满足它们。这种性质就是所谓的不变式。在多数情况中，这些不变式涉及系统中的多个组件，是横贯它们的性质。相应的证明称为不变式保持性证明。
状态和事件
正如我们在前一节里已经看到的，一个离散迁移组件包括一个状态和若干迁移。我们现在用一些简单的术语来说明有关情况。
粗略地说，状态（如同在一个命令式程序里一样）由一些变量表示。但是，与程序里的情况不同，这里的变量可以是整数、偶对、集合、关系、函数等（也就是说，可以是任何集合论里可以表示的数学对象），而不仅是计算机里的对象（即那些受限的整数和浮点数、数组、文件一类的东西）。除了变量定义外，我们可能还有不变式语句—它们可以用任何在一阶逻辑和集合论的描述范围内能够写出的谓词表示。把所有这些放在一起，一个状态就可以简单地抽象为一个集合。
练习：在一个人可以按动一个按钮的离散系统里，状态是什么？在一个发动机可以启动和停止的系统里，状态又是什么？
根据上面的所有说法，一个事件可以抽象为状态空间上一个简单的二元关系。该关系表示了顺序的前后两个状态之间的联系，这两个状态中的一个恰好出现在该事件的“执行”之前，另一个恰好出现它之后。当然，直接把事件定义为二元关系，有可能不太方便。更好的方式是把事件分解为两个部分，一些卫和一些动作。
卫也就是一个谓词，一个事件的所有卫并在一起，就得到了与之对应的二元关系的作用域。一个动作也就是对状态变量的一次简单赋值。假定一个事件的所有动作将同时在不同的变量上“执行”，未赋值的变量不会改变。
这些也就是我们在定义状态迁移系统时使用的全部记法形式。
练习：在一个人可以按动一个按钮的离散系统里，有哪些事件？在一个发动机可以启动和停止的系统里，又有哪些事件？在这两个系统之间可能有哪些关系？
在这个工作阶段，我们可能会有点困窘—发现最后一个问题不太容易回答。事实上，从一开始，我们就没有遵照“药方”。或许我们应该先写下一个与用户/按钮/发动机有关的定义和需求文档。在做这件事时，我们可能就已经发现了，发动机和按钮之间的关系原来并不是那么简单。在这里可能出现下面一些问题：我们究竟需要一个按钮，还是几个按钮（例如，一个开始按钮和一个停止按钮）？后一做法是一个好想法吗？如果采用多个按钮，在发动机已经运转的情况下再按启动按钮，我们会观察到什么？在这种情况下，我们是否必须松开按钮以便随后重新启动发动机？如此等等。我们也可能看清楚了，与其分别考虑一个按钮系统和一个发动机系统，而后再组合它们，更好的做法可能是先将其作为一个问题来考虑，而后再分解成几个。这时，我们又要考虑，怎么在这两者之间放进去一点软件，如此等等。
横向精化和证明 要想模拟一个包含很多离散迁移组件的大系统，这样的工作当然不可能一蹴而就，只能通过一系列的工作步骤来完成，在每一步中把这个模型做得更丰满一点。我们首先创建其各种组件的状态和迁移，而后再充实它们；先以非常抽象的方式，而后引入更具体的元素。这种活动称为横向精化（或者 superposition，叠加）。在做这种事情时，系统工程师会仔细考察定义和需求文档，逐渐从中提取出一些元素来进行形式化。他们还要关心模型里的定义和需求的可追溯性。注意，经常会出现这样的情况，我们在建模中会发现定义和需求文档是不完全的或不一致的，因此需要对它们做相应的编辑修改。在应用这种横向精化方法时，我们也需要做一些证明，确保更具体的精化步骤不违背在更抽象的精化步骤中已经完成的工作。这就是精化证明。
最后，当模型中每个定义和每个需求都被考虑了之后，横向精化阶段就完成了。在做横向精化的过程中，我们并不关心可实现性。我们的数学模型，就是用集合论的记法形式描述的状态不变式和状态迁移。
在做横向精化时，我们将通过增加变量的方式扩充模型的状态，也可以强化事件的卫或者增加新的卫，还可以给事件增加新的动作。最后，还可以增加新的事件。
纵向精化和证明 还有第二类精化工作，这类工作在所有横向精化完成之后才能执行。鉴于这种情况，这时我们不会在模型里加入任何新细节，只是转换离散系统里的某些状态或迁移，以使它们更容易在计算机上实现。这种精化称为纵向精化（或者数据精化）。这类精化常常可以用一个半自动化的工具来做。这样做时，同样需要做精化证明，以保证实现选择与更抽象的观点吻合。
纵向精化的典型实例，如把有穷的集合转换为布尔数组，同时把各种集合运算（并、交、包含等）对应地转换为一些程序循环。
在执行纵向精化时，我们可以删去一些变量并加入一些新变量。纵向精化中的一个重要方面是所谓的连接不变式，它建立起具体状态和抽象状态之间的联系。
通信和证明 建模工作有一个非常重要的方面，与未来系统中不同组件之间的通信有关。在顺序地完成一系列精化时，我们必须在这方面非常小心。一开始就按照组件在最终系统里所具有的通信方式建模它们之间的通信，是一种错误的做法。做这件事的更好方法是，首先设想每个组件都有“权利”去直接访问另一些组件的状态（这仍然是非常抽象的考虑）。这样做就是搞了一点“欺骗”，显然，在现实中情况不可能是这样。但是，把这种方法用在初始的横向精化步骤里，是非常方便的做法，因为随着精化步骤的进展，组件将和它们之间的通信一起逐步精化，逐渐变得更加充实。只有到了最后的横向精化步骤，我们再根据组件之间的真实通信模式引入对应的各种通道。这样做才是最合适的，也能把全局系统分解为一些相互通信的子系统。
在此之后，我们还需要弄清楚，在每个组件看到其他组件的状态的模糊图景时，应该如何针对它们的状态迁移做出的反应。出现这种情况，是因为消息在组件之间传递需要一点时间。因此，我们必须证明，即使出现了这样的时间偏移，所有事情“仍然像”不存在这种时间偏移的情况一样。这是我们需要完成的另一类精化证明。
能做到无缺陷：这是什么意思？
现在我们已经可以准确地说明，所谓的“无缺陷”系统究竟意味着什么了。这个词语，如本序言的标题所言，反映了我们的最终目标。
设想一个控制火车网络的程序，如果它不是采用“构造即正确”的方式开发出来的，那么我们在写出它之后，肯定无法证明该程序能保证不会出现两列火车相撞的情况。这时再去证明这一性质，已经太晚了。这时我们能测试或证明的，只是诸如这个程序在做数组访问时不会出现越界，或者不会出现危险的空指针访问，或者不存在算术溢出的危险（这件事貌似很简单，但请记住，这也就是导致阿丽亚娜 5 型火箭在其首次航行中爆炸的问题，事先没有检查出来）。我们应该看到在问题的解的认证和问题的认证之间的差异，这件事非常重要。看起来，这里存在着值得注意的混乱，许多人并没有清晰地区分这两种不同的认证工作。
解的认证只关心构造出来的软件，有关工作就是针对上面提到的一些软件性质（数组越界访问、空指针、溢出等）确认这个软件没有问题。与之对应的，问题的认证关注的是系统的全局情况（例如，保证列车在一个给定的铁路网中总能安全运行）。在做这件事情时，我们必须证明整个系统（不仅是其中的软件）的所有组件都能和谐地参与到完成这一全局目标的活动中。
要证明程序保证两列火车绝不会相撞，我们就必须通过模拟这个问题的方式来构造程序。显然，这个问题中的一个重要部分就是需要考虑的性质，它们必须是作为工作之始的那个模型的一部分。
自然，我们也应该注意，有时人们可以成功地做出某些类别的问题证明，作为得到的解（程序）的一部分。人们完成这一工作的方式，通常是在程序里加入一些幽灵变量（ghost variable），以此处理需要考虑的问题。在最终的程序里，这类变量将被删除。我们认为，这种方法是过于人为的赘物。其主要缺点是，它只能关注软件的情况，不能关注更广泛的问题。事实上，幽灵变量的这种使用，恰恰说明需要在问题层面上做抽象的推理。本书中倡导的方法正是从抽象开始，对它们做推理，后来再引入程序。
在模型开发的横向精化阶段，我们将会考虑很多性质。在横向开发阶段结束时，我们应该已经精确地知道了，这种不会撞车的性质到底是什么意思。在做这些工作的过程中，我们要精确地给出所有假设（尤其是有关环境的假设），有了这些，模型就能保证两列火车绝不会相撞。
正如我们已经看到的，有关的性质本身是不够的。通过展示出所有假设，我们才能做好问题的认证。从本质上说，这种做法与仅仅针对软件能做的事情完全不同。
采用这一类方法，我们就能在开发结束时断言，相对于系统需要的所有性质，系统一经构造出来就是无缺陷的。在这种情况下，我们把所考虑的“缺陷”是什么都精确地说清楚了（而且特别是弄清了有关的假设）。
当然，我们也应该注意到一种微妙的情况。在前面的讨论中，我们佯装说明这种方法能做出最终的软件，使它相对于它的环境是构造即正确的。换句话说，这一全局系统是无缺陷的。完成这一工作的方式，就是在我们构造的环境里建模，并在此过程中完成一些证明。前面说过，这一环境由设备、物理现象、一些软件以及用户等组成。显然，这些元素不可能完全地形式化。因此，与其说软件相对于它的环境是正确的，更恰当一点，不如说它的正确性是相对于我们在此之前构造出的那个环境模型的。显然，该模型只是物理环境的一个近似。如果这个近似与真实环境的距离很远，那么软件就可能在一些事先未曾预料的外部情况中出错。
综上所述，我们只能佯装说完成了一个相对无缺陷的构造，而非绝对的，因为后者根本不可能。当这个解还在婴儿期时，我们就要找到一种方法，做出一个环境的模拟，使其是真实环境的一个“很好的”近似。显然，概率性方法一定对这类工作很有用。
关于证明
此前我们曾几次提到，需要在建模的过程中完成一些证明。首先，我们显然需要有一个工具来自动生成那些必须证明的东西。让人自己明确写出所有必须证明的形式化语句，显然是很愚蠢的（也太容易出错了）。对于很简单的系统，常常也需要做数以千计的证明。其次，我们也需要能自动完成证明的工具：在这方面的典型情况是，90%以上的证明都可以自动完成。
这里出现了一个有趣的问题，那就是需要研究在自动证明失败时究竟发生了什么情况。导致失败的可能因素有：①自动证明器不够聪明；②要求证明的语句本身为假；③需要证明的语句本身是不可证明的。对于情况①，我们必须做交互式的证明（参看后面的“工具”部分）；对于情况②，这个模型应该做一些重要的修改；对于情况③，这个模型需要充实。情况②和③都非常有趣，它们正好说明了，证明活动对于建模所可能扮演的角色，就像是测试相对于程序的角色。
还应注意，最终能自动证明的百分比，也是模型质量的一个很好的指示器。如果需要做太多的交互式证明，可能说明这个模型太复杂。通过简化模型，我们常常可以大幅度地提高自动完成的证明的百分比。
设计模式 设计模式近年来非常走红，也是由于多年前的一本针对面向对象软件开发的设计模式著作 [3]。但是，实际上，这个想法本身比那本书里谈到的更具普遍性：它可以很有成效地扩展到任何特定的工程专业领域，特别是系统工程领域，就像这里所设想的。
有关想法就是先写下一些预定义的小的工程处方，只要根据不同的场景对它们做相应的统一的实例化，就可以重复地使用它们。对于我们的情况，这种模式在形式上就是一些经过证明的参数化模型，它们可以被结合到各种大项目里。这样做的优势是可以避免重复证明，只做一次，而后就能重复地用在基于模式的开发中。我们有可能开发出相应的工具，帮助我们以系统化的方式方便地完成模式的实例化和组合。
动态演示
这里还有一个很奇怪的东西：之前我们强烈建议把正确性的保证构筑在建模和证明的基础上。而在这一小节，我们则准备说，“动态演示”（即“执行”）模型可能也是一个“很好的”主意。
当然，前面我们一直认为，有数学就足够了，因此并不需要执行。这里有什么矛盾吗？是不是我们实际上并不能确定数学处理已经足够了，或者无法保证数学总是“真的”？并非如此！在证明了毕达哥拉斯定理之后，任何数学家都不会再想去通过度量一个直角三角形的两条直边和斜边来验证这个定理！那么，为什么我们要去执行模型呢？我们确实已经证明了一些东西，并对自己的证明也确信无疑。但是，我们怎么能简单地确信已经证明的就是需要证明的东西呢？这里可能有些事情是很难接受的：我们（花了很多力气）写下了定义和需求文件，就是出于一个原因，想弄清楚需要证明些什么。而我们现在又说，或许该需求文档说的并不是我们真正需要的东西。确实，情况就是这样，历史并不总是直线前进的。
直接演示已有的模型（在这里，我们没有说再去做某种特殊的模拟，而是直接使用已经建立的模型），并在屏幕上展示整个系统（而不仅是其中的软件部分）的活动情况，用以检查我们写出的东西正是自己所需，也是一种非常有效的方法。经常会出现这样的情况：在做动态演示时，我们发现以前所写的需求文档并不足够精确，或者它要求了某些不必要的性质，甚至发现它要求的某些性质并不符合实际需要。
动态演示是建模的补充，它能帮助我们发现一些问题，使我们能在早期阶段修改自己的想法。更有意义的是，做这些的代价并不大，远远低于通过对最终系统做了一次实际执行，竟然发现我们构造出的系统并不是自己想要的东西（实在是太晚了）。
看起来，动态演示似乎应该在证明之后再做，作为编程阶段之前的一个额外工作阶段。这不对！我们的想法是，应该在横向精化阶段里尽可能早做一些动态演示，甚至在非常抽象的层面上做。这样做的理由是，如果我们必须修改需求（并重做一些证明），最重要的就是确切地知道模型中的哪些部分可以保留，模型结构的哪些地方应该修改。
同时进行演示和证明还有另一个正面作用。回忆一下，我们说过，证明也是一种找出和排除模型中错误的方法：一个证明不能完成，可以看作模型里有“错误”，或者是模型过于贫乏的一种指示剂。一个不变式保持证明做不出来，也有可能在证明之前就通过演示揭露出来，并且得到了解释。通过演示，我们很容易发现无死锁的反例。但也请注意，动态演示并不意味着我们可以暂时把证明活动停下来，上面的讨论只是想说，它可以是证明的一个非常有用的补充。
工具
对于开发正确的系统而言，工具非常重要。我们建议，在这里已经有了一个（形式化的）包含着模型的正文文件及其一系列精化之后，我们应该离开常规的工作方式。按我们的建议，需要有一个数据库，用于记录和处理建模的对象，如模型、变量、不变式、事件、卫、活动，以及它们之间的关系，这些都是我们在前面提到过的。常规的静态分析器能处理这些组件，完成词法分析、名字冲突检查、数学式的正文语法分析、精化规则的验证，如此等等。
根据上面的讨论，最重要的工具之一称为证明义务生成器。它能分析已有的模型（不变式、事件等）以及它们的精化，生成需要证明的语句。
最后，还需要某些证明工具（自动化的和交互式的），以便能消解前一工具生成的那些证明义务。在这里，我们应该理解一个重要的情况：这里需要执行的证明，并不像专业的数学家需要去攻克（或感兴趣）的那一类证明。我们的工具应该考虑这个情况。在一项数学研究中，数学家的兴趣就是去证明一个定理（例如四色定理）以及一些引理（例如 20 个引理）。数学家不会想利用数学的帮助去构造出一个人造物件。在数学项目中，研究的问题是不变的（始终就是那个四色定理）。
在一个工程项目中，有数以千计的定理需要证明。进一步说，在开始时，我们并不清晰地知道需要证明什么。还要注意的是，我们不是要证明火车绝不相撞，而要证明，在有关环境的某些确定假设之下，所构造的系统能确保火车不会相撞。我们要证明的东西涉及有关构造过程中我们对问题的认识，以及工作过程（并非线性的）的进展情况。
作为这种情况的推论，一个工程证明器可能需要一些功能。对专门帮助数学家做证明的工具而言，这些功能可能没必要。这里提出两种功能：差分式的证明（在模型做了少许修改之后，如何找出哪些证明需要重做）；存在无用假设下的证明。
除了我们在这一部分讨论的工具集，如果再增加一些使用同一个核心数据库的工具，也可能很有价值：动态演示工具、模型检验工具、UML 转换工具、设计模式工具、组合工具、分解工具，等等。这意味着，工具系统应该按有利于扩充的方式来构造。按照这种设计哲学开发的一个工具就是 Robin 平台，可以从 Event-B 官方网站免费下载。
遗产代码问题
遗产代码带来两方面问题：①我们希望开发一部分新的软件，而这部分软件需要连接某些遗产代码；②我们希望修复或更新某些遗产代码。
问题①最常见，在开发所有新代码时，几乎都会遇到这个问题。在这种情况下，遗产代码也就是新产品的环境中的一个元素。这里的挑战是，如何能模拟遗产代码的可观察行为，以便把它纳入模型中，就像处理环境里的其他元素一样。要做好这件事，在新产品的需求文档里，就必须包含一些与遗产代码有关的元素。这种需求（假设）必须首先非形式化地定义清楚，就像前文解释的那样。
工作中的目标，应该是为模型开发出与有关遗产代码兼容的最小接口。与通常的情况一样，关键还是抽象和精化：这样才能逐步把遗产代码引入模型，采用的方式应使我们能顾及它所提供的具体接口的各个方面。
与问题①相比，问题②要困难得多。事实上，这种修复更新经常带来非常令人失望的结果。人们趋向于认为，遗产代码本身“就是”在修复更新中应该使用的需求文档。这种看法完全是错误的。
首先，我们应该写出一个全新的需求文档，定义好抽象的需求，使之独立于在遗产代码中看到的具体实现。即使它偏离了遗产代码，也不应该犹豫。
其次，修复更新遗产代码，工作方式是开发并证明它的一个模型。这里的危险是过于接近地模仿遗产代码，因为它可能包含一些不好理解的方面（除了编写遗产代码的程序员通常都不在场之外），而且它显然不是通过形式化建模方法开发出来的。
我们的建议是，在开始这种修复更新之前多加斟酌。更好的方法是开发一个新产品。一些人认为开发新产品的代价可能高于简单更新，但是，经验说明情况可能并不如此。
集合论记法的使用 物理学家或运筹学家们也构造各种模型，但他们绝不为了这些工作去发明新的语言，而是始终使用经典的集合论记法形式。
计算机科学家则不然，因为他们接受的教育就是做程序，所以常常相信需要为建模发明新的语言。这也是一个错误。集合论记法形式非常适合做我们需要的系统模拟，而且更重要的是，我们也完全能理解自己写下的语句是什么意思！
经常听到这样一种说法，说是必须隐藏起数学的表达形式，因为工程师不能理解它，也害怕它。这完全是一派胡言。我们能设想，在设计一个电力网络时，由于电力工程师可能害怕数学记法，就必须隐藏起数学的表达形式吗？
其他认证方法 目前存在着许多不同的软件认证方法，包括测试、抽象解释和模型检验等。
这些方法都是认证问题的解（相应的软件），而不是认证问题（全局的系统）。在每种情况中，我们都是先构造出一部分软件，然后（也仅仅是然后）再设法去认证它（模型检查并不完全是这种情况，它也被用于认证问题）。为了完成认证工作，我们考虑清楚所期望的性质，并通过检查，认定该软件确实具有这些性质。如果情况不是这样，我们就必须去修改软件，而这样做经常又会引入更多的问题。众所周知，这种方法代价高昂，远远大于纯粹开发的代价。我们不认为独立地使用这些方法是很合适的，当然，我们也不拒绝它们。我们要说的是，这些方法有可能成为建模和证明方法的补充。
创新
大型的工业公司通常都很难搞创新。当然，他们有时也想做这件事，拿出一大笔钱来专门用于搞创新。不用说，这种情况很罕见。大家也都知道，大公司的所谓研发（R&D）部门并不能为其业务部门提供任何有意义的新技术。
虽然如此，融资机构仍竭尽全力，希望与此类大公司的实际研究计划建立关系。这是错误的。他们更应该与那些更小一些的创新活动建立联系。
我相信，把这里倡导的方法介绍给业界，应该更多地通过小型的创新性公司，而不是通过那些大公司。
教育
今天涉足大型软件项目的大多数人都没得到正确的教育。公司一般认为，编程工作可以由层级较低的人来做—他们没有或者很少有数学的基础和兴趣（常见情况是程序员并不喜欢数学，这就是他们选择做计算的首要原因）。所有这些都很糟糕。对于一个系统工程师而言，最基本的基础就是一种良好（或更高）水平的数学教育。
计算是第二个问题，应该在已经很好地理解了必要的数学基础之后。如果不能做到这些，这个领域就不可能进步。当然，事情也很清楚，许多专业人员不同意这种说法，这也不是我们面临的最小的问题。许多专业人员仍然对计算和数学感到困惑。
与一大批缺乏适当水准的教育的人们相比，“维护”较少的经过良好教育的人们，需要付出的代价更低。这并不是一种精英的观点。谁会认为，一名医生或建筑师，不需要接受其专业领域的正确教育，就能把工作做得很好？再说一次，系统和软件工程师的最基础的训练就是（离散）数学。
未来的软件工程师必须学习两个特殊的科目：写需求文档（在实际软件工程的教学计划中，极少出现这一科目）；构造数学模型。在这方面，基本方法是非常面向实际的。在教授这些科目时，教师应该让学生完成很多实例和项目。经验说明，对于一个已经有良好的数学基础的学生而言，掌握数学方法（包括证明）不会是一个问题。技术转移
把这一类技术转移到业界，可能是一个严重的问题。根本原因就在于管理者极其不情愿改变自己的开发过程。通常，这些过程很难定义，更难付诸实践。这也是管理者不希望改变它们的原因。
在开发过程中，结合进一个重要的写需求文档的初始阶段，随后是另一个重要的建模阶段，通常会被认为是很危险的，因为这些新加的阶段将在项目开始期间强行地加入可观的代价。再说，管理者并不相信，早期的这种付出意味着后期的节约。然而，经验说明，这样做将能显著地降低整体成本，因为后面测试阶段的高昂代价显著地降低了。类似的还有修补设计错误带来的巨大工作量。
在所有这些之上，为了把一种技术转移到工业界，我们需要做的初始工作就是在教育领域里努力进取。没有这种初始努力，任何技术转移的企图都注定要失败。还应该注意到，也存在一些欺骗性的技术转移。在那里，人们假装使用某种形式化的方法（虽然实际上没有用），实际上只是某些权力部门想给软件加上某种“形式化”标签。
本文摘自刚刚上架的《Event-B建模 系统和软件工程》
Event-B建模 系统和软件工程
[法] 简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial） 著，裘宗燕 译
- 国际著名计算机科学家简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial）著
- 以Event-B方法开创者的角度阐释软件需求形式化建模技术
- 通过逐步精化来完成系统建模和设计。
这本实用的教科书适用于形式化方法的入门课程或高级课程。本书以B形式化方法的一个扩展Event-B作为工具，展示了一种完成系统建模和设计的数学方法。
简-埃蒙德•阿布瑞尔（Jean-Raymond Abrial）是国际著名计算机科学家，曾任苏黎世联邦理工学院客座教授，他基于精化的思想提出了一种系统化的方法，教读者如何逐步构造出所期望的模型，并通过严格的证明完成对所构造模型做系统化的推理。本书将介绍如何根据实际需要去构造各种程序，以及如何更为普遍地构造各种离散系统的模型。本书提供了大量的示例，这些示例源自计算机系统开发的各个领域，包括顺序程序、并发程序和电子线路等。
本书还包含了大量具有不同难度的练习和开发项目。书中的每个例子都用Rodin平台工具集证明过。
本书适合作为高等院校计算机、软件工程、网络工程、信息安全等专业高年级本科生、研究生的教材，也可供相关领域的研究人员和技术人员参考。