J-R.Abrial_FM_ICES2006 阅读笔记

J-R.Abrial_FM_ICES2006 阅读笔记

文章概述

该篇文章简要地概述了用B形式化的两个实际的项目, 主要是说明一种"构造即正确"的思路, 并且分析了其中的困难和优势.

首先是形式化方法, 利用形式化方法可以将需求文档转换成可执行代码, 但是是在一种抽象的层次进行, 所以没有执行的概念, 我们并不可以对这些代码进行执行和调试.

将开发途径划分为3个阶段:

• 从需求文档中抽取细节, 构造抽象模型
• 利用抽象模型转换到一个具体模型
• 将具体模型翻译成可执行代码

整体效果是得到的可执行代码是构造即正确的.

关于抽象模型, 它是包含数据的, 同时包含用简单转换来描述的动态特性.

关于证明, 工程师可以通过数学证明的方法来验证他们正在构造的抽象模型, 需要证明的语句不用工程师自己定义, 而是有证明义务生成器的工具自动生成.

证明关注两方面情况:

• 抽象模型里的转换是否保持了不变式的成立
• 抽象模型的每一个更准确的版本是否破坏了前一个版本已经证明的性质, 称为精化性证明

关于具体模型, 和抽象模型一样, 也由数据和转换构成,

• 是从抽象模型里的抽象集合论结构到计算机的集合论对象的数据精化
• 将基于集合论的非确定性转化, 转换到经典的确定性的程序设计语句

关于可执行代码

• 具体模型被自动地翻译为所需要的形式, 采用某种经典的程序设计语言.
• 用一个普通编译器, 将由具体模型生成的程序语言版翻译成可执行代码.

关于需求文档的重要性:

• 其质量通常较差, 或者是太短, 或者是相反, 太罗嗦. 遇到这两种情况, 要提取精确的 需求都很难. 应该清楚, 使用软件形式化方法并不能更正软件需求文档里的问题. 换句话说, 如果需求文档里存在一个错误或一项疏漏, 该错误或疏漏也很可能出现在抽象模型里. 注意, 无论如何, 对抽象模型做各种证明可以揭示出软件需求文档里一些不一致性.
• 抽象模型开发者对需求文档的理解里可能出现错误, 使抽象模型没有反映软件需求文档 作者的意图. 这一问题可以部分地通过组织一个复审小组（独立于开发小组）的方式处理, 该小组的工作就是检查抽象模型, 以确认它正确反映了软件需求文档的内容. 这一队伍在两 个案例中都起了重大的作用.

关于抽象模型的难点

使用形式化方法，困难的部分肯定是在构造抽象模型时遇到的。一般而言，工程师（特别 是软件工程师）并没有经过有关建模训练方面的良好教育，如前一节指出的，他们在软件需 求文档的撰写方面也没有良好的训练

关于测试

• 定义手头要测试的程序的某个精确属性
• 详尽描述测试的预期结果，需要在测试之前做好。注意，有时很难得到这种详尽描述， 因为它必须有某种根据，而且显然这一根据应该独立于被测试的程序。然而在一些时候，作 为测试依据的详尽描述的根据就出自测试者的头脑，是测试者通过查看程序究竟做了些什么 而得到的
• 测试本身是由被测试的程序运行
• 比较测试结果与测试前预期的详尽描述的结果。测试结果与预期结果相同并不意味着这 个程序是正确的，而仅仅意味着它通过了测试。如果比较的结果是否定的，我们可以认为是 这个程序不正确，也可以认为是所预期的结果不正确

阅读感悟

这篇文章从两个案例入手, 详细地分析了两个案例的具体细节, 给出其中的异同点, 随后对开发工作中的许多要点进行了分析, 例如需求文档, 抽象模型的难点等, 对测试和证明给出了较为完善的解释, 并对证明中的各类情况进行了一定的讨论和分析. 进一步介绍了使用EdithB进行具体模型的构造和精化, 最后总结了开发过程的集成等, 并对形式化的更多应用进行了一定的概括