[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

为什么软件工程师必须知道形式化方法？ 

程京德

    “软件工程”是为了保证大规模软件系统的高可靠性，研究以系统化的、规范化的、可量化的、过程化的工程方法去定义、设计、开发和维护大规模软件系统，以及如何将这些方法应用到工程实践的工程专业学科。

    由美国联邦航空管理局(FAA)及国家航空和宇宙航行局(NASA)联合发布的一份调查报告中阐述道：“形式化方法应该是每个计算机科学家和软件工程师教育的一部分，正如应用数学的适当分支是所有其他工程师教育的必要部分一样(Formal methods should be part of the education of every computer scientist and software engineer, just as the appropriate branch of applied mathematics is a necessary part of the education of all other engineers)”。

    电子数字计算机是“逻辑机器”，计算机程序是“逻辑指令序列”，要保证程序在计算机上运行结果的100%正确性，唯一有效的办法就是以逻辑学及数学为基础对程序进行正确性验证。这是一个在原理上非常容易理解但是在实践中极其难以贯彻执行的道理。

    荷兰计算机科学家  Edsger Wybe Dijkstra 在1970年说过一段非常著名的话：“程序测试可以用来显示缺陷的存在，但永远不能显示缺陷的不存在！( Program testing can be used to show the presence of bugs, but never to show their absence!)”[1]  在其1972年图灵奖获奖演说中，Dijkstra 再次强调说明了他的主张：“今天，通常的技术是制作一个程序，然后测试它。但是：程序测试可能是显示缺陷存在的一种非常有效的方法，但是对于显示缺陷的不存在来说是无可救药的。显著提高程序可信度的唯一有效方法是给出令人信服的正确性证明。( Today a usual technique is to make a program and then to test it. But: program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness.)”[2,3]。

    Dijkstra 对程序验证在软件工程中之本质重要性的提倡，是软件工程形式化方法的发端，尽管 C. A. R. Hoare 曾经说过“软件验证的起源可以追溯到计算机科学的先驱冯诺依曼和图灵。(The origins of software verification go back to the pioneers of Computing Science, von Neumann and Turing. )”。

    牛津大学出版社计算机科学词典中如下定义形式化方法：“一种基于数学和逻辑的框架，用于规定、开发和验证系统。形式化方法通常允许系统被视为或表示为一个数学公式。因此，它们使分析者能够证明一个规范是可行的(可以被实现)，证明一个实现是正确的，并且证明一个系统的属性，而不需要实际执行它。形式化方法通常包括两个主要元素：一个形式语言或规范语言，以及一个涉及演绎机制的验证系统。(A mathematically and logically based framework for specifying, developing, and verifying systems. Formal methods typically allow a system to be viewed or represented as a mathematical formula.  Hence, they enable an analyst to prove that a specification is feasible (can be implemented), to prove that an implementation is correct, and to prove the properties of a system without actually executing it. A formal method generally comprises two main elements: a formal language or specification language, and a verification system involving a deductive apparatus.)”[Dictionary of Computer Science (7th Ed.), OUP]

     自 Dijkstra 对程序验证在软件工程中之本质重要性的提倡之后，已经有许多计算机科学家在形式化方法领域做了大量工作，提出了许多方法论，研发了许多自动化支持工具。

    1997年，NASA Langley 研究中心的 Holloway 对以往文献中所强调的、对支持使用形式化方法进行软件开发的论证进行了一次广泛调查并做了一个逻辑分析，归纳提出了一个比各种经典论证更简单、更有力的一个替代论证：“软件工程师都想努力成为真正的工程师，真实的工程师都使用适当的数学，因此软件工程师也应该使用适当的数学，然而形式化方法是软件的数学，所以软件工程师都应该使用合适的形式化方法。”[4]  简单！精辟！有说服力！[微笑😊]

    1996年，国际标准化组织颁布了 VDM 形式化方法的国际标准：International Standard ISO/IEC 13817-1, Information technology - Programming languages, their environments and system software interfaces - Vienna Development Method - Specification Language - Part 1: Base language, 1996-12.

    2002年，国际标准化组织颁布了形式化规格描述语言 Z 的国际标准：International Standard ISO/IEC 13568, Information technology - Z formal specification notation — Syntax, type system and semantics, 2002-07-01.

    知道形式化方法国际标准并且自觉运用形式化方法的思想于日常软件开发工作中，应该是每个职业软件工程师的最基本素质。

    能够在软件开发工作中熟练地使用形式化方法国际标准以及自动化工具，应该是开发高可靠性大规模软件系统的每个职业软件工程师的不可或缺之必要职业技能 [实际上，掌握这一技能的程度已经成为国外(欧美日)国内职业软件工程师之间的巨大差距]。

    本文为笔者多年来讲授“软件工程形式化方法”课程中对学生们说明形式化方法之重要性的内容之拔萃，提供给有兴趣的读者参考。

参考文献

[1] E. W. Dijkstra, “Notes on Structured Programming,” 1970.

[2] E. W. Dijkstra, “The Humble Programmer,” ACM Turing Award Lecture, 1972. 

[3] 程京德,“ACM 图灵奖历届获奖者 - 1971-1975”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2023年4月8日。

[4] C. M. Holloway, “Why Engineers should Consider Formal Methods,” 1997.

微信公众号“数理逻辑与哲学逻辑”