J-R.Abrial_FM_ICES2006 阅读笔记

J-R.Abrial_FM_ICES2006 阅读笔记

文章概述

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

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

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

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

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

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

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

证明关注两方面情况:

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

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

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

关于可执行代码

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

关于需求文档的重要性:

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

关于抽象模型的难点

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

关于测试

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

阅读感悟

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

本文参与腾讯云自媒体分享计划,欢迎正在阅读的你也加入,一起分享。

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏python学习之旅

算法学习笔记(二):贪心算法

1923
来自专栏WOLFRAM

版本11.2——追求极致的极限

2124

使用粒子群优化器来解决旅行商人问题

粒子群优化器,作为一种使用人工智能来解决问题的方式,在解多元、恒变的方程式方面有很大的优势。在本文中我们主要讲的是通过修改算法来解决一些问题,例如使用离散固定值...

2567
来自专栏AI研习社

MIT Taco 项目:自动生成张量计算的优化代码,深度学习加速效果提高 100 倍

我们生活在大数据的时代,但在实际应用中,大多数数据是 “稀疏的”。例如,如果用一个庞大的表格表示亚马逊所有客户与其所有产品的对应映射关系,购买某个产品以 “1”...

36111
来自专栏PPV课数据科学社区

【学习】如何用SPSS和Clementine处理缺失值、离群值、极值?

一、什么是预处理、预分析? 高质量数据是数据分析的前提和分析结论可靠性的保障。尽管在获取数据源时数据分析师格外谨慎,耗费大量的时间,但数据质量仍然需持续关注。不...

9465
来自专栏数说工作室

哈希函数的套路 | 文本分析:大规模文本处理(1)

这个系列打算以文本相似度为切入点,逐步介绍一些文本分析的干货。 第一篇中,介绍了文本相似度是干什么的; 第二篇,介绍了如何量化两个文本,如何计算余弦相似度,穿...

4658
来自专栏AI科技大本营的专栏

实战 | 让机器人替你聊天,还不被人看出破绽?来,手把手教你训练一个克隆版的你

编译 | AI科技大本营(rgznai100) 参与 | 史天 聊天机器人到底是什么呢?说白了,就是计算机程序通过听觉或文本方法进行对话。 当今最流行的四个对话...

4058
来自专栏AI科技评论

开发 | MIT Taco项目:自动生成张量计算的优化代码,深度学习加速效果提高100倍

AI科技评论消息:我们生活在大数据的时代,但在实际应用中,大多数数据是“稀疏的”。例如,如果用一个庞大的表格表示亚马逊所有客户与其所有产品的对应映射关系,购买某...

37911
来自专栏AI科技评论

开发丨深度学习框架太抽象?其实不外乎这五大核心组件

许多初学者觉得深度学习框架抽象,虽然调用了几个函数/方法,计算了几个数学难题,但始终不能理解这些框架的全貌。 为了更好地认识深度学习框架,也为了给一些想要自己亲...

3694
来自专栏新智元

【干货】谷歌 TensorFlow Fold 以静制动,称霸动态计算图

【新智元导读】谷歌日前推出深度学习动态图计算工具 TensorFlow Fold,可以根据不同结构的输入数据建立动态的计算图,简化训练阶段输入数据的预处理过程,...

3483

扫码关注云+社区

领取腾讯云代金券