软件工程形式化方法初学体会

本贴最后更新于 1649 天前,其中的信息可能已经时过境迁

最近在上一门叫做新技术讲座的课,我估计好多同学是看到讲座这两个字感觉这课会很水才选的,但实际上这门课讲的内容是非常硬核的软件工程形式化方法,而且授课老师也是国内第一批研究软件工程形式化方法的教授,现任日本埼玉大学教授,且上课非常认真负责,每节课都有课堂练习。不过了解了软件工程形式化的概念后,发现这个研究方向真的了不得,简直可以颠覆整个软件行业。

在早期的软件开发过程中,开发者们往往拿到问题后就直接开始编码,软件往往会出现各种各样的问题,大部分软件的质量十分低下,被称为“软件危机”。为了解决软件质量低下的问题,人们提出了软件工程化的思想,也就是目前主流的软件开发方式,引入了从需求分析到最后编码实现这一系列的过程,以及需要遵守的一系列规范,并定义了如 CMMI 这样的规范性等级。然而软件工程里面有很多内容的规范是非常主观的,没有一个确定的评定标准,另外很多步骤只能尽量争取正确,但根本无法确保正确,比如对于软件的测试,在软件测试这门课中就了解到全覆盖基本上是不可能完成的,并提出了语句覆盖、判定覆盖、条件覆盖等一系列只能尽量争取正确的测试覆盖。而且在执行的过程中,就算是 CMMI 5 级的开发单位也往往会为了追求进度而省去其中某些甚至很多步骤,导致最后开发出来的软件根本不可用。可以说,软件工程化确实解决了一部分问题,但治标不治本,没有从根本上解决软件质量低下的问题。

有没有一种方法可以从根本上解决问题呢?有,就是软件工程形式化方法。软件工程形式化的目的简单来说就是把要解决的问题先用逻辑学和集合论等数学的方式把它抽象表示出来,也就是形式化,之后就可以自动化的方式完成一些原本需要大量人工完成的步骤。它的效果是可以减少软件开发的成本,同时大大减少软件中的错误。由于数学是稳定的、抽象的,可以应用到各个领域,可以作为一个相对正确性的基础,因此我们就可以将其他事物的正确性建立在数学的正确性之上。另外,形式化方法可以大大减少规格说明的二义性,防止出现客户和开发方对需求理解不一致的情况。我们可以这么理解,在软件工程形式化方法中,只要规格说明(specification) 是正确的,那么最后的软件产品一定是正确的,甚至连测试都不需要做。就如同建筑一样,只要图纸和设计方案正确,那么一个合格的施工队一定能建造出正确的建筑,而且已经建造完毕的建筑也无法像软件产品一样测试之后发现错误再进行修改。

为何建筑工程的精准性和正确性如此之高,其实就是引入了形式化方法的思想。在建筑工程设计中,一定都会首先在图纸上对建筑进行力学分析和计算,确保最终建筑拥有完美的力学结构,或者至少不容易塌。并且设计单位和施工单位往往不是同一家,但最后的施工成果依然能满足设计单位原先的要求。而在软件工程中,对于数学的应用主要在算法、数据结构中,比较少地用来抽象具体事物以及约束它们的关系。从这个角度看软件开发过程的先进性远远不如建筑工程的过程,尽管 IT 被认为是高新技术。

在软件工程形式化方法中,规格说明的重要性大大提高了,同时在规格说明中,如何用数学语言而不是自然语言抽象一个具体的事物是需要重点考虑的问题。可以看一下伦敦地铁线路图的抽象例子。
老图:伦敦地铁原图.PNG
新图:伦敦地铁新图.PNG

可以看到最后抽象的结果十分清晰明了、没有歧义、且具有可维护性,与之相比,老图尽管更精确地反应了真实的地理位置,但却让读者感到混乱。目前几乎所有城市的地铁以及公交线路示意图都模仿了伦敦地铁图。软件工程形式化的规格说明也需要像这样排除无关事物的干扰,并且精准、无二义性。比如,“令 x=3,y=x+1”就比“令 x 为一个存有 3 的内存单元,令 y 为存有 x+1 的值的内存单元”好得多,尽管在计算机中实际运算的过程可能是后一种。

在软件工程形式化方法中,是不需要进行测试的,尽管利用形式化方法产生测试用例同样可以提高效率,而且工业应用上也有相应的工具,但实际上并不推荐这样的用法。因为测试本质上就是效率低下的,前面已经提到,测试根本无法保证所有可能的结果都正确。在软件工程形式化方法中,取代测试地位的是证明(proof)。绝大多数关于软件工程形式化方法的文章中都提到了证明,可见证明在软件工程形式化方法中的重要性。证明可以保证的正确性远远高于测试。工程师在构建抽象模型的过程中,需要通过数学证明的方式逐步验证它。要证明的语句不需要工程师自己定义,而是由一个叫做证明业务生成器的工具自动生成。为了生成证明语句,该工具将不断分析抽象模型的各个精化形式。要做的证明需要关注两方面情况:1.抽象模型里的转换是否保持了不变式的成立。这方面称为不变式保持证明。2.抽象模型的每个更准确的版本是否破坏了前一版中已经证明的性质,这称为精化正确性证明。这些证明中的大多数都由一个叫做证明器的工具自动完成。

当然,任何方法都不是十全十美的,软件工程形式化方法也存在着一些问题以及推广上的障碍。尽管软件形式化方法总体上来说能够节省成本,但它在前期设计规格说明阶段投入较多,传统观念根深蒂固的老板们可能这样做觉得不值得。对于软件工程师来说,习惯了传统的开发方式,而软件形式化方法需要换一种思路去思考问题,可能前期不太适应,而且对于非数学专业的他们来说,对系统构造出清晰的数学关系模型可能稍显困难。另外,则是形式化方法中用到的自动化工具本身可能存在问题,无法保证翻译器能够正确地将数学模型翻译成可执行代码,这样也就无法保证最终的正确性。

尽管如此,但从软件工程形式化目前已有的应用来看,它是相当成功的。最早的软件工程形式化方法应用是在 IBM 的 CICS 系统中。当时 CICS 的复杂程度已经成了一个严重的问题,靠人力已经很难再对这个系统进行维护,因此 IBM 想要重新设计这个系统。当时 CICS 的经理和牛津大学的一名研究形式化方法的教授进行了沟通,并决定使用形式化方法来重新设计 CICS 系统,使用的方法叫做 Z notation。工程师们习惯了使用自然语言来描述 specification,一开始还担心用数学方法来表示 specification 对他们来说很困难。但最后证明这并不是个问题,就连没有一些数学经验的程序员也能够轻松运用。最终开发成本减少了百分之 9,用户报告的错误减少了 2.5 倍,而且都是轻微的错误。巴黎地铁 14 号线和 Roissy 机场穿梭车的无人运行系统也是使用形式化方法开发的。它们使用的方法叫做 B notation,比 Z notation 出现得更晚一些。这两个案例都没有执行单元测试,工程师没有修改任何代码行,然而最终的运行结果仍然非常成功。

软件工程形式化方法的前景十分远大,一旦实现在工业中的广泛应用,将彻底颠覆整个软件行业,大幅度提高生产效率和减少错误。非常有幸能在大学中了解到这么前沿的技术。

相关帖子

欢迎来到这里!

我们正在构建一个小众社区,大家在这里相互信任,以平等 • 自由 • 奔放的价值观进行分享交流。最终,希望大家能够找到与自己志同道合的伙伴,共同成长。

注册 关于
请输入回帖内容 ...

推荐标签 标签

  • 钉钉

    钉钉,专为中国企业打造的免费沟通协同多端平台, 阿里巴巴出品。

    15 引用 • 67 回帖 • 381 关注
  • LeetCode

    LeetCode(力扣)是一个全球极客挚爱的高质量技术成长平台,想要学习和提升专业能力从这里开始,充足技术干货等你来啃,轻松拿下 Dream Offer!

    209 引用 • 72 回帖
  • 七牛云

    七牛云是国内领先的企业级公有云服务商,致力于打造以数据为核心的场景化 PaaS 服务。围绕富媒体场景,七牛先后推出了对象存储,融合 CDN 加速,数据通用处理,内容反垃圾服务,以及直播云服务等。

    25 引用 • 215 回帖 • 160 关注
  • Sandbox

    如果帖子标签含有 Sandbox ,则该帖子会被视为“测试帖”,主要用于测试社区功能,排查 bug 等,该标签下内容不定期进行清理。

    362 引用 • 1212 回帖 • 580 关注
  • 酷鸟浏览器

    安全 · 稳定 · 快速
    为跨境从业人员提供专业的跨境浏览器

    3 引用 • 59 回帖 • 21 关注
  • 安全

    安全永远都不是一个小问题。

    189 引用 • 813 回帖 • 2 关注
  • 百度

    百度(Nasdaq:BIDU)是全球最大的中文搜索引擎、最大的中文网站。2000 年 1 月由李彦宏创立于北京中关村,致力于向人们提供“简单,可依赖”的信息获取方式。“百度”二字源于中国宋朝词人辛弃疾的《青玉案·元夕》词句“众里寻他千百度”,象征着百度对中文信息检索技术的执著追求。

    63 引用 • 785 回帖 • 249 关注
  • 微信

    腾讯公司 2011 年 1 月 21 日推出的一款手机通讯软件。用户可以通过摇一摇、搜索号码、扫描二维码等添加好友和关注公众平台,同时可以将自己看到的精彩内容分享到微信朋友圈。

    129 引用 • 793 回帖 • 1 关注
  • 思源笔记

    思源笔记是一款隐私优先的个人知识管理系统,支持完全离线使用,同时也支持端到端加密同步。

    融合块、大纲和双向链接,重构你的思维。

    18150 引用 • 66978 回帖
  • Caddy

    Caddy 是一款默认自动启用 HTTPS 的 HTTP/2 Web 服务器。

    10 引用 • 54 回帖 • 126 关注
  • TextBundle

    TextBundle 文件格式旨在应用程序之间交换 Markdown 或 Fountain 之类的纯文本文件时,提供更无缝的用户体验。

    1 引用 • 2 回帖 • 45 关注
  • CAP

    CAP 指的是在一个分布式系统中, Consistency(一致性)、 Availability(可用性)、Partition tolerance(分区容错性),三者不可兼得。

    11 引用 • 5 回帖 • 552 关注
  • 持续集成

    持续集成(Continuous Integration)是一种软件开发实践,即团队开发成员经常集成他们的工作,通过每个成员每天至少集成一次,也就意味着每天可能会发生多次集成。每次集成都通过自动化的构建(包括编译,发布,自动化测试)来验证,从而尽早地发现集成错误。

    14 引用 • 7 回帖
  • DevOps

    DevOps(Development 和 Operations 的组合词)是一组过程、方法与系统的统称,用于促进开发(应用程序/软件工程)、技术运营和质量保障(QA)部门之间的沟通、协作与整合。

    37 引用 • 24 回帖 • 1 关注
  • Wide

    Wide 是一款基于 Web 的 Go 语言 IDE。通过浏览器就可以进行 Go 开发,并有代码自动完成、查看表达式、编译反馈、Lint、实时结果输出等功能。

    欢迎访问我们运维的实例: https://wide.b3log.org

    30 引用 • 218 回帖 • 594 关注
  • Ubuntu

    Ubuntu(友帮拓、优般图、乌班图)是一个以桌面应用为主的 Linux 操作系统,其名称来自非洲南部祖鲁语或豪萨语的“ubuntu”一词,意思是“人性”、“我的存在是因为大家的存在”,是非洲传统的一种价值观,类似华人社会的“仁爱”思想。Ubuntu 的目标在于为一般用户提供一个最新的、同时又相当稳定的主要由自由软件构建而成的操作系统。

    123 引用 • 168 回帖
  • RIP

    愿逝者安息!

    8 引用 • 92 回帖 • 284 关注
  • Angular

    AngularAngularJS 的新版本。

    26 引用 • 66 回帖 • 498 关注
  • LaTeX

    LaTeX(音译“拉泰赫”)是一种基于 ΤΕΧ 的排版系统,由美国计算机学家莱斯利·兰伯特(Leslie Lamport)在 20 世纪 80 年代初期开发,利用这种格式,即使使用者没有排版和程序设计的知识也可以充分发挥由 TeX 所提供的强大功能,能在几天,甚至几小时内生成很多具有书籍质量的印刷品。对于生成复杂表格和数学公式,这一点表现得尤为突出。因此它非常适用于生成高印刷质量的科技和数学类文档。

    9 引用 • 32 回帖 • 178 关注
  • Vue.js

    Vue.js(读音 /vju ː/,类似于 view)是一个构建数据驱动的 Web 界面库。Vue.js 的目标是通过尽可能简单的 API 实现响应的数据绑定和组合的视图组件。

    261 引用 • 662 回帖 • 1 关注
  • 禅道

    禅道是一款国产的开源项目管理软件,她的核心管理思想基于敏捷方法 scrum,内置了产品管理和项目管理,同时又根据国内研发现状补充了测试管理、计划管理、发布管理、文档管理、事务管理等功能,在一个软件中就可以将软件研发中的需求、任务、bug、用例、计划、发布等要素有序的跟踪管理起来,完整地覆盖了项目管理的核心流程。

    5 引用 • 15 回帖 • 223 关注
  • Unity

    Unity 是由 Unity Technologies 开发的一个让开发者可以轻松创建诸如 2D、3D 多平台的综合型游戏开发工具,是一个全面整合的专业游戏引擎。

    25 引用 • 7 回帖 • 248 关注
  • HHKB

    HHKB 是富士通的 Happy Hacking 系列电容键盘。电容键盘即无接点静电电容式键盘(Capacitive Keyboard)。

    5 引用 • 74 回帖 • 402 关注
  • FreeMarker

    FreeMarker 是一款好用且功能强大的 Java 模版引擎。

    23 引用 • 20 回帖 • 427 关注
  • 微软

    微软是一家美国跨国科技公司,也是世界 PC 软件开发的先导,由比尔·盖茨与保罗·艾伦创办于 1975 年,公司总部设立在华盛顿州的雷德蒙德(Redmond,邻近西雅图)。以研发、制造、授权和提供广泛的电脑软件服务业务为主。

    8 引用 • 44 回帖
  • 知乎

    知乎是网络问答社区,连接各行各业的用户。用户分享着彼此的知识、经验和见解,为中文互联网源源不断地提供多种多样的信息。

    10 引用 • 66 回帖
  • jsDelivr

    jsDelivr 是一个开源的 CDN 服务,可为 npm 包、GitHub 仓库提供免费、快速并且可靠的全球 CDN 加速服务。

    5 引用 • 31 回帖 • 33 关注