B方法-拓展你形式化方法的视野
B方法-拓展你形式化方法的视野
写在前面
最近忙着写软件体系结构论文,才开始了解所谓的形式化方法。形式化方法在软件开发中有其特殊地位,了解一下对于计算机程序生涯,将有所裨益,下文将以直观形式介绍一下形式化方法,尤其是B方法。
当然从这篇博客起,我将保持简洁,崇尚头脑风暴,更详细的展开不在此处讨论。
1 什么是形式化方法?
使用非形式化的自然语言描述系统规格说明容易引起二义性,不完整,可能存在矛盾;为了克服欠形式化方法的缺点,人们把数学引入软件开发过程,创造了基于数学的形式化方法。
所谓形式化方法,是指具有坚定数学基础的方法(例如集合,关系,谓词逻辑等)的基础之上的方法,是数学上的综合,分析技术的应用,用于开发计算机控制的系统,经常有推力工具的支持,它可以提供一个用于模型设计和分析的严格而有效的途径。
简而言之,形式化方法即建立在严格数学基础之上的软件设计,验证,并运用与实际开发的技术。
目前流行的形式化方法,包括有穷自动机,Petri网,Z语言,上下文相关的文法等形式化方法。
2 形式化方法直观感受
Z方法和B方法均由法国科学家Jean-Raymond Abrial发明,B方法基于集合,关系和谓词逻辑等数学理论书写规范,主要通过不变式(INVARIANT)和证明义务(Proof Obligation, PO)来保证规范正确性。B方法描述软件的基本单元是抽象机(Abstract Machine),抽象机之间可以组织成更大的抽象机,抽象机可以逐步精化直至最终实现。
典型的抽象机组织结构如下图所示:
下面通过B方法直观感受下形式化方法开发。这里的例子来自北大数学系 裘宗燕教授B方法课件(你可以访问裘宗燕老师关于B方法的课程主页了解更多内容)。
B方法的支持工具软件AtelierB如下图所示。
我们展示的是一个银行叫号机的简化模型EnumMachine,它包括三个操作:
1)客户下一个号码takeNext操作
2)银行服务员服务下一客户的的叫号serveNext操作
3)号码重置操作reset操作。
我们需要编写的叫号机的模型,在B方法中称之为抽象机,代码如下图所示:
上述这段代码中IF语句以及其他逻辑关系符号,表示了简单的数学关系以满足叫号机的正确性。这里只是作为展示,其实形式化方法可以包含更多的逻辑性以满足程序正确性,而且不都是用我们熟悉的if..else语句表示的。
编写完的抽象机需要进行类型检查,然后由系统自动或交互式完成证明义务,系统生成的证明义务如下图所示:
类型检查通过后,免费版的AtelierB可以为我们生成一个叫号机模型的C语言头文件,如下图所示:
根据生成的头文件,由开发人员完成实际代码的编写,当然其他版本的AtelierB可以支持生成更多语言的代码,从抽象机到自动代码生成,我们看到了B方法的强大能力。
3 形式化方法特点
形式化方法克服了非形式化语言描述的缺点,它能简洁准确地描述研究对象,便于建立正确完整的数学规则说明;同时在软件开发过程中使用数学的另一个有点是,可以在软件工程活动之间平滑地过渡,不仅功能规则说明,系统设计也可以使用数学表达式,当然程序代码也是一种数学符号。可以利用数学证明方法证明设计符合规则说明,程序代码正确地反映了设计结果。当然形式化方法也绝不是万灵神药,他也有它的局限性,因此也有人对形式化方法持怀疑态度。
对于形式化方法我接受两个观点:
1)软件需求日益复杂,软件开发过程中没有一个普适的解决问题的方法,因此任何有助于缓解系统复杂性,提高软件质量的方法都有其价值;
2) 不要过分夸大某一种方法的能力,没有绝对的正确与先进,计算机技术总是不断发展的,实践中总是结合多种方法的优势进行的。
好了吧,头脑风暴就到这儿了,如果对形式化方法感兴趣,想进一步学习,下面你需要思考诸如数组是一个索引到值的函数(映射)之类的数学问题了。
B方法-拓展你形式化方法的视野相关推荐
- 软件工程——形式化方法概述
目录 前言 一.形式化方法定义 二.形式化方法分类 三.形式化方法意义 四.形式化方法作用 五.形式化方法优缺点 1.优点 2.缺点 前言 形式化方法英文的名称是formalmethods,形式化方法 ...
- 阅读和了解什么是形式化方法?
1.形式化方法概念: 形式化方法英文的名称是formal methods.在逻辑科学中是指分析.研究思维形式结构的方法.它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互 ...
- 1、阅读和了解什么是形式化方法 2、推荐阅读书籍《大象——thinking in UML》
什么是软件形式化方法 软件形式化方法是指建立在严格数学基础上的软件开发方法.形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明.形式化方法使软件开发人员可以应用严格的数学符号来说明.开发和验 ...
- 鉴于现有的形式化方法(简称“桥”系列)有其优点和缺点,特发明新的“秤”系列
鉴于现有的形式化方法及其形式化语言(简称"桥"系列)具有的优点和缺点, 特依据信息基本定律发明新的"秤"系列,以扩充并解决"桥"系列所解决不 ...
- 阅读和了解什么是形式化方法
形式化方法就是在逻辑科学中是指分析.研究思维形式化结构的方法.它把各种具有不同内容的思维形式加以比较,找出其中各个部分互相联结的方式.如果一个方法有良好的数学基础,那么它就是形式化的,典型的以形式化规 ...
- 阅读和了解什么是形式化方法,推荐月的书籍《大象---thinking in UML》
形式化方法,中文也称形式方法.正规方法.在计算机科学和软件工程领域,形式化方法是基于数学的特种技术,适合于软件和硬件系统的描述.开发和验证.将形式化方法用于软件和硬件设计,是期望能够像其它工程学科一样 ...
- 《融智学进阶文集》01:间接计算模型和间接形式化方法
<融智学进阶文集>01: 间接计算模型和间接形式化方法 01-间接计算模型和间接形式化方法_邹晓辉.pdf 怎么采用融智学七遍通方法熟悉原创文本? 对照阅读 摘要: 本文旨在:从人机交互界 ...
- 形式化方法、《大象:Thinking in UML》
形式化方法英文的名称是formal methods.在逻辑科学中是指分析.研究思维形式结构的方法.它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包 ...
- 【形式化方法:VDM++系列】4.VDM实战1——铁路费用计算
又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完 ...
- 形式化方法|形式化方法对软件开发的挑战:历史与发展
几年前到某著名大学参加学术活动,无意中听到该校两位老师闲聊,现在还记得的一句话就是"形式化方法已经不行了".看来真是隔行如隔山,评价自己不熟悉的领域,而且随便说,难免出错.在对形式 ...
最新文章
- head和tail命令详解
- HTML的标签描述20
- 用FIO测试存储性能
- 磁盘及文件系统管理(三)
- ABCpdf.NET 的简易使用指南
- 图解分析一个dNet进销存软件
- 摘自《读者》的哲理短句——赞美篇
- OpenCV学习笔记资料大集锦
- go语言接收html上传的文件,html5原生js拖拽上传(golang版)
- springmvc重定向到另一个项目_SpringMVC——redirect重定向跳转传值
- Apache Tomcat 5.5 Servlet/JSP 容器
- Windows使用技巧
- 用SQL Server Compact Edition创建移动应用程序 【转载】
- 容器化单页面应用中RESTful API的访问
- html里写js ajax吗,js、ajax、jquery的区别是什么?
- python语言的三个主要特点_python干货|新总结的4个python语言的特点,这几个细节值得关注...
- quadprog函数的介绍和应用,二次规划函数
- 获得系统异常的详细信息
- 获取properties文件的内容的几种方式
- Eclipse中集成SVN
热门文章
- 解放生产力「GitHub 热点速览 v.21.51」
- 达梦数据库/DM7迁移之导出sql脚本
- 7段均衡器最佳参数_十段均衡器的设置和参数
- 麻瓜编程python爬虫微专业_网易微专业麻瓜编程Python Web开发工程师教程
- MySQL 5.7 参考手册(官方中文版) | 2.2 安装和升级MySQL
- mysql 8.0 手册
- 微机原理 寻址方式 及基于EMU8086的用例
- 小米高通9008授权服务+Miflash(fh_loader.exe)脚本刷机_icloudelectron
- win10配置Android SDK环境变量
- Vulkan Loader 何时加载 ICD 驱动文件