Event-B建模_（法）简·埃蒙德·阿布瑞尔（Jean-Raymond Abrial）著.pdf

序言：无缺陷系统？我们能！这个标题当然很有桃衅的味道。我们都会认为，这一宣言是针对着某些不可能的事情。不可能！环视四周，我们还做不出无缺陷的系统。如果这件事有可能，应该早就被人们做好了。再说，无论如何，我们首先要说清楚什么是“缺陷”。我们该怎么想象这里的情况呢？我们可能想，这应该是一位大师想兜售他最新的灵丹妙药。亲爱的读者，请放心，这个序言并不包含任何全新的克敌法宝，而且进一步说，它也不是技术性的，不要求你理解一大堆复杂的概念。本序言的意图，就是提醒你注意一些简单的事实和想法。如果愿意，你就可以去利用它们。这里的思路就是去扮演某个人的角色，这个人现在正面临一种险恶的局面（是的，计算机化的系统的开发并没有远离险境一作为一种度量的尺度，只需要考虑在系统崩溃时所浪费的金钱)。在面临险境时，我们有可能决定以某种鲁莽的方式去改变某些东西。但是，这样做通常完全无效。另一条途径就是逐步引入一些简单的特征，希望把它们放在一起最终能导致局面的全局性改变。后者也就是我们将要用在这里的“哲学”。定义和需求文档我们的目标就是构造出正确的系统，因此，首先需要认真地定义一种方法，据此可以判断自己做出的东西究竞是什么。这就是“定义和需求”文档的用途。在投身于开发一个计算机化的系统之前，必须认真地写出这种文档。但是，你会说，大量工业部门都有这种文档，它们已然存在，为什么还要为此操心呢？好吧，就我个人的经验，绝大多数情况是，业界正在使用的文档非常糟糕。仅仅是理解需求到底是什么，将其从有关文档中提取出来，通常就已经很困难了。一个事实是，人们常以做文档时用了某些（昂贵）工具的事实作为其需求文档值得信任的证据！我强烈建议，应该按照本节中说明的简单路线重写需求文档。这样的一个文档应该包含两类相互嵌套的正文：解释性的正文和参考性的正文。前者包含为理解手头问题所需要的解释，当读者第一次遇到这里的问题，或者需要某些基本的理由时，这些解释应该能帮助他们。后者包含定义和需求，其形式主要是带有标签和编号、用自然语言写出的简短陈述句。与相应的解释相比，这种定义或需求应该更形式化。当然，它们必须是自足的，而且能成为判断正确性的唯一参考。定义和需求文档应该类似于数学书籍，其中一段段的解释性文字（在这里，作者非形式化地解释自己的方法，有时还给出一些历史背景)里交织着一些更形式化的片段一定义、引理和定理一所有这些构成了参考性正文，很容易与书中的其他内容区别开来。对于系统工程的情况，我们用两个坐标来标记参考性的定义和需求。第一个坐标说明其