“形式化方法应该是每个计算机科学家和软件工程师教育的一部分，正如应用数学的适当分支是所有其他工程师教育的必要部分一样。(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.)”  -- FAA (Federal Aviation Authority) and NASA (National Aeronautics and Space Administration), USA

现代软件工程的根本目的是保证大规模软件系统的高可靠性。软件工程的终极目标是自动程序设计及自动软件开发，而自动程序设计及自动软件开发的必要前提是软件需求定义及软件规格的形式化表达。软件工程形式化方法应该是支撑整个现代软件工程的理论基础。

本文目的为劝诱有志成为专业软件工程师的软件工程或相关专业本科生研究生在校读书期间选修《软件工程形式化方法》课程，告诫学生们不选修该课程将来工作后一定会后悔。文章采用问答方式，直击要害，不多废话。

“软件工程”是什么？

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

“形式化方法”是什么？

“形式化方法是软件工程方法，它应用严谨的、基于数学的符号和语言来规范、开发和验证软件。通过使用规范语言，可以系统地检查软件模型的一致性（或无歧义性）、完整性和正确性，检查过程可以是自动的，也可以是半自动的。”[1,2]

“软件工程”为什么重要/必要？

因为现代信息社会的国防、金融、医疗、交通、通信等核心基础领域都深度依赖于大规模软件系统，而大规模软件系统开发面临复杂度高、需求多变、质量难以把控的现实难题，未经工程化管控的软件开发必然导致需求偏离、质量失控与维护成本爆炸，所以软件工程通过规范化工程化手段管控开发全流程，以此保障软件产品可靠、高效且可维护，是非常必要的。[1-4]

“形式化方法”为什么重要/必要？

因为形式化方法能够使用严格的数理逻辑方法在软件开发的需求定义、规格描述、系统设计、程序自动生成、系统验证等各个阶段都精确刻画系统行为、消除自然语言带来的歧义漏洞，并且可以使用自动化验证工具检查系统是否100%满足需求及规格，所以它对保障高可靠软件系统的一致性、完整性、正确性、安全性、可维护性是非常必要的。[1-4]

“大语言模型工具”能够根据人类简单提问自动生成无歧义的100%正确的软件需求定义吗？

因为人类的简单提问本身往往含有模糊、隐含、主观的信息，并且大语言模型本质上是基于概率预测而非绝对无误的逻辑推理，缺乏对现实世界特定真实业务景情的真实理解，所以它不能够仅凭人类的简单提问自动生成无歧义的100%正确的软件需求定义。

“大语言模型工具”能够将自然语言描述的软件需求定义自动转换成为无歧义的100%正确的形式化需求定义吗？

因为自然语言需求本身就潜藏歧义、隐含假设与业务约束，从自然语言需求到形式化需求定义的转换依赖于对模糊语义和隐性约束的精确形式化抽象表达，大语言模型难以完整捕获全部真实业务逻辑且存在生成虚构风险，导致其在从自然语言到形式规约的转换中面临语义偏离、逻辑不可判定等挑战，所以它不能够自动转换成为无歧义的100%正确的形式化需求定义。

“大语言模型工具”能够将形式化需求定义自动转换成为形式化规格描述吗？

尽管可以假设形式化需求定义已经逻辑完备，因为形式化需求与形式化规格描述分属不同抽象层次（前者刻画系统“是什么，做什么”，后者规定“如何精确实现”），形式化需求到形式化规格描述的转换涉及复杂的逻辑映射、嵌套模态捕捉以及严格的语法约束，且大语言模型存在虚构现象，无法保证严格遵守形式体系的全部约束，所以大语言模型工具不能无条件自动转换得到完全正确的形式化规格描述。

“AI编程”能够保证100%的程序正确性吗？

因为大语言模型本质上是基于概率预测的文本生成器，缺乏对真实业务逻辑的深层理解，缺乏严密的逻辑验证与确定性保障，并且在处理边界条件、异常状态及并发场景时存在固有的表层正确性与虚构缺陷，所以AI编程不能够保证100%的程序正确性。

“AI编程”能够保证系统一致性和完整性吗？

因为AI编程难以完整理解系统全部隐含约束、全局业务逻辑，AI编程依赖局部概率生成而非对整体架构的确定性逻辑推理与形式化验证，容易引入模块间的语义冲突与状态隐患，容易产生局部正确但全局冲突的输出，所以AI编程不能够保证系统的一致性和完整性。

“AI编程”能够保证软件可维护性吗？

因为AI编程主要基于局部上下文进行片段化的代码生成，缺乏对软件整体架构演化及重构的全局规划/预测能力，并且AI编程生成的代码容易出现模块边界模糊、过度冗余、编程风格混乱、程序注释缺失、文档不完备，所以AI编程不能够保证软件可维护性。

为什么说“形式化规格驱动”是软件工程永远的范式？

因为软件工程的本质是解决人类意图需求的模糊性与计算机执行的精确性之间的鸿沟，所以形式化规格驱动作为唯一能用严谨的数理逻辑精准地规定系统正确性约束条件、消除二义性的手段，成为跨越这一鸿沟并保障高可靠软件系统质量的永恒基石，为开发、验证与演化提供可靠基准，所以 “形式化规格驱动” 是软件工程永远的范式。

为什么说“形式化方法”是AI编程时代软件工程师的“必备看家本领”？

因为大语言模型工具永无可能进行正确逻辑推理[5]，人工智能永无可能全面超越人类智能[6]，世界上最珍贵最可靠的智力资源永远是人类自身，尤其是其中之佼佼者。大规模软件系统是人类社会永远必须的基础设施，其高可靠性永远是第一位重要的要求。只有掌握了形式化方法的软件工程师才能为软件系统开发及维护整个软件生涯周期提供基于逻辑基础的方法论支持，为软件系统高可靠性提供根本保障。所以，形式化方法是AI编程时代软件工程师的“必备看家本领”。

“形式化方法”不仅仅是软件工程必要的方法论理论基础，实际上也是信息安全性工程必要的方法论理论基础，笔者将另文介绍。

（2026年8月13日记）

参考文献

[1] 程京德,“为什么软件工程师必须知道形式化方法？”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年9月26日。为什么软件工程师必须知道形式化方法？

[2] 程京德,“为什么软件工程专业应该将《软件工程形式化方法》设置为必修课？”，微信公众号“数理逻辑与哲学逻辑”，2025年12月23日。为什么软件工程专业应该将《软件工程形式化方法》设置为必修课？

[3] 程京德,“数理逻辑学的重要性，兼论计算机/人工智能学院设置数理逻辑学必修课之必要性”，微信公众号“数理逻辑与哲学逻辑”，2025年12月20日。数理逻辑学的重要性，兼论计算机/人工智能学院设置数理逻辑学必修课之必要性

[4] 程京德,“AI 编程时代软件工程形式化方法的必要性：挑战、范式转移与研究展望”，微信公众号“数理逻辑与哲学逻辑”，2025年12月5日。AI 编程时代软件工程形式化方法的必要性：挑战、范式转移与研究展望

[5] J. Cheng, “Why Cannot Large Language Models Ever Make True Correct Reasoning?”arXiv:2508.10265 [cs.AI], https://doi.org/10.48550/arXiv.2508.10265, 16 August 2025; PhilArchive, https://philpapers.org/archive/CHEWCL-3.pdf, 15 June 2026;  程京德，“Why Can’t LLMs Ever Make True Correct Reasoning - Introduction, Reasoning, Logical Basis, Limitations”，微信公众号“数理逻辑与哲学逻辑”，2025年8月9日，2025年8月10日，2025年8月11日，2025年8月15日； 程京德，“Why Can’t LLMs Ever Make True Correct Reasoning? (revision)”，微信公众号“数理逻辑与哲学逻辑”，2025年8月24日，2026年6月16日(增补)。Why Can't LLMs Ever Make True Correct Reasoning? (revision)

[6] 程京德，“人工智能永无可能全面超越人类智能”，微信公众号“数理逻辑与哲学逻辑”，2025年7月5日。人工智能永无可能全面超越人类智能