形式化方法——裘宗燕课程讲义

来源：北京大学裘宗燕《程序设计语言原理》课程中的”形式化方法”章节讲义（2006年2月—6月），共4页。

1. 软件开发的本质性问题

软件的本质性问题是复杂性和多样性：
- 极端的复杂性：可能具有成百万甚至成千万行规模
- 异常丰富多彩的应用需求，需求的不断提升和变化
- 组成部分之间异常复杂的直接与间接相互作用方式
- 静态结构与动态性质之间难以把握的复杂关系
软件开发的现实困境：
- 项目经常延误，不能按期完成
- 经常超出预算
- 后期发现前期设计错误，更正代价高昂
- 发布的软件中存在许多错误，时常崩溃
- 维护和更新代价非常高
没有灵丹妙药——任何不幼稚的计算机工作者都不应期望有朝一日能发明某种新技术一劳永逸地解决软件开发难题

2. 形式化方法的定义与核心活动

形式化方法研究如何把具有清晰数学基础的严格性（描述形式、技术和过程）融入软件开发的各阶段：

活动	说明
Specification（规范）	采用具有严格定义的形式和语义的记法，描述软件设计（和实现）
Reasoning and Analysis（推理和分析）	对形式化规范进行分析和推理，确定静态和动态性质——是否一致完整？有无矛盾遗漏？运行中是否出现不可容忍状态（死锁、活锁）？
Refinement（精化）	从抽象的高层描述，严格保证语义一致地推导出更接近实现的规范，最终得到正确实现了高层规范的可运行程序（逐步求精的严格化）

3. 朴素方法 vs 形式化方法 vs 半形式化方法

方法	基础	语义	可检查性
朴素方法	自然语言的思考、设计和描述	语义含糊，可能有歧义	无法严格检查，只能通过人的交流
形式化方法	严格定义的数学概念和语言	语义清晰，无歧义	可开发自动化工具进行检查和分析
半形式化方法（如 UML）	较清晰定义的形式和部分语义	语义较清晰	可能开发工具进行一些检查和分析

趋势：软件开发正在从朴素的、非形式的设计方法，向着更加严格、更加形式化的方向转变。

4. 形式化方法的实践与应用

编译器领域：词法/语法分析和语义处理是形式化方法早期最成功的范例——从文法描述自动生成分析器
安全攸关系统：核电站监控、武器系统、交通调度、铁路信号、交通工具控制、医疗设备控制等
经典案例：
- IBM CICS Control System（1980年代末，Using Z）
- 法国高速铁路控制系统（B方法，J-R Abrial）
- AMD K5 浮点除法运算正确性证明（1990年代）
- 模型检查技术在硬件领域成为标准技术（Intel 奔腾芯片浮点错误的教训）
规范文档中的应用：
- RBAC 2004 规范中采用形式化规范语言 Z
- W3C WSDL 2.0、XPath 2.0 Formal Semantics 采用形式化描述
- Windows 2000 基于形式化模型的程序分析工具找出数以万计的错误和漏洞

5. Z 语言简介

Z 语言由法国计算机科学家 J-R Abrial 在 1980 年前后于牛津大学程序研究组（PRG，Hoare 领导）提出
基于一阶谓词逻辑和集合论的形式化规范描述语言
有严格定义的数学理论基础，规范简明、精确、无歧义
属于面向模型的方法（基于状态的方法）：从已知的简单抽象数学对象出发，构造目标系统的状态特征和行为特征模型
基本抽象数学对象包括：数据元素、元组、集合、包（bag）、序列、映射（函数）
类似方法：VDM、B 等

6. 常见质疑与回应

质疑	回应
没有形式化方法，不也做出了许多软件吗？	社会运转越来越依赖计算机系统，没有良好质量保证的软件不应继续存在
我没学过形式化方法，也做了许多程序	掌握了形式化方法的思想和技术，有可能做得更好；不了解将来会发现许多东西看不懂
形式化方法太难了	程序本身也是形式化描述，通常比抽象层次上的形式化描述复杂得多；新型工具将降低应用难度
形式化方法有什么用？	断言、前/后条件、循环不变式、基于契约的开发、净室技术等都基于形式化方法的研究成果

7. 形式化方法的局限

非形式的客观需求与形式化规范之间的关系，不可能形式地处理
形式化规范较难阅读，具备形式化训练的专业人员较缺乏
实际证明比较复杂，需要强有力的工具支持
支持工具仍然比较缺乏，功能不够丰富，界面和交互方式不够友好
不能保证不出现错误，只是在这些方面有所帮助

关联笔记

本讲义属于裘宗燕《程序设计语言原理》课程的一部分，可与云盘中其他程序设计语言相关资料关联
Z 语言的进一步学习可参考：Jim Woodcock and Jim Davis, Using Z —— Specification, Refinement and Proof；J. M. Spivey, Z Reference Manual