收藏 分享(赏)

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

上传人:sc****y 文档编号:78301 上传时间:2023-02-18 格式:PDF 页数:491 大小:74.52MB
下载 相关 举报
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第1页
第1页 / 共491页
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第2页
第2页 / 共491页
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第3页
第3页 / 共491页
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第4页
第4页 / 共491页
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第5页
第5页 / 共491页
Event-B建模_(法)简·埃蒙德·阿布瑞尔(Jean-Raymond Abrial)著.pdf_第6页
第6页 / 共491页
亲,该文档总共491页,到这儿已超出免费预览范围,如果喜欢就下载吧!
资源描述

1、序言:无缺陷系统?我们能!这个标题当然很有桃衅的味道。我们都会认为,这一宣言是针对着某些不可能的事情。不可能!环视四周,我们还做不出无缺陷的系统。如果这件事有可能,应该早就被人们做好了。再说,无论如何,我们首先要说清楚什么是“缺陷”。我们该怎么想象这里的情况呢?我们可能想,这应该是一位大师想兜售他最新的灵丹妙药。亲爱的读者,请放心,这个序言并不包含任何全新的克敌法宝,而且进一步说,它也不是技术性的,不要求你理解一大堆复杂的概念。本序言的意图,就是提醒你注意一些简单的事实和想法。如果愿意,你就可以去利用它们。这里的思路就是去扮演某个人的角色,这个人现在正面临一种险恶的局面(是的,计算机化的系统的

2、开发并没有远离险境一作为一种度量的尺度,只需要考虑在系统崩溃时所浪费的金钱)。在面临险境时,我们有可能决定以某种鲁莽的方式去改变某些东西。但是,这样做通常完全无效。另一条途径就是逐步引入一些简单的特征,希望把它们放在一起最终能导致局面的全局性改变。后者也就是我们将要用在这里的“哲学”。定义和需求文档我们的目标就是构造出正确的系统,因此,首先需要认真地定义一种方法,据此可以判断自己做出的东西究竞是什么。这就是“定义和需求”文档的用途。在投身于开发一个计算机化的系统之前,必须认真地写出这种文档。但是,你会说,大量工业部门都有这种文档,它们已然存在,为什么还要为此操心呢?好吧,就我个人的经验,绝大多

3、数情况是,业界正在使用的文档非常糟糕。仅仅是理解需求到底是什么,将其从有关文档中提取出来,通常就已经很困难了。一个事实是,人们常以做文档时用了某些(昂贵)工具的事实作为其需求文档值得信任的证据!我强烈建议,应该按照本节中说明的简单路线重写需求文档。这样的一个文档应该包含两类相互嵌套的正文:解释性的正文和参考性的正文。前者包含为理解手头问题所需要的解释,当读者第一次遇到这里的问题,或者需要某些基本的理由时,这些解释应该能帮助他们。后者包含定义和需求,其形式主要是带有标签和编号、用自然语言写出的简短陈述句。与相应的解释相比,这种定义或需求应该更形式化。当然,它们必须是自足的,而且能成为判断正确性的唯一参考。定义和需求文档应该类似于数学书籍,其中一段段的解释性文字(在这里,作者非形式化地解释自己的方法,有时还给出一些历史背景)里交织着一些更形式化的片段一定义、引理和定理一所有这些构成了参考性正文,很容易与书中的其他内容区别开来。对于系统工程的情况,我们用两个坐标来标记参考性的定义和需求。第一个坐标说明其

展开阅读全文
相关资源
猜你喜欢
相关搜索

当前位置:首页 > 教育教学 > 其它

copyright@ 2008-2023 wnwk.com网站版权所有

经营许可证编号:浙ICP备2024059924号-2