形式化方法（Z 语言）课程系列 — 裘宗燕 2006
北京大学数学学院裘宗燕老师 2006 年 2-6 月”形式化方法”研究生课程讲义，共 7 讲 + 1 个实例研究（归并自云盘 8 个 PDF，约 234 页）。课程挂靠在其”程序设计语言原理”课程体系下，参考书为 Woodcock & Davis《Using Z》和 Spivey《Z Reference Manual》。
第 1 讲：引言 — 为什么需要形式化方法
- 软件的本质问题是极端复杂性 + 多变性：百万行规模、需求持续变化、组成部分间直接/间接交互难以把握。软件是人类有史以来最复杂的人工制品。
- 类比”设计 vs 制造”：传统开发前期成果全是自然语言”文档”，只有最终程序是形式化的——从非形式文档到复杂程序的跨越距离太大，关系无法保证。形式化方法把严格描述提前到设计阶段。
- 形式化方法三要素：
- Specification（规范）：用严格定义形式和语义的记法描述软件设计与实现；
- Reasoning & Analysis（推理分析）：检查一致性、完整性、有无死锁/活锁、找缺陷；
- Refinement（精化）：从抽象描述语义一致地逐步推导出可运行程序（逐步求精的严格化）。
- 实践成功案例：编译程序自动生成（BNF→自动机，最成功范例）；IBM 用 Z 对 CICS 做再工程；法国 Transport 公司用 B 方法开发高铁控制系统；AMD K5 浮点除法形式化证明；模型检查成硬件设计标准技术；基于形式化模型的静态分析在 Windows 2000 找出数以万计漏洞；RBAC 2004、W3C WSDL 2.0/XPath 2.0 规范直接采用 Z。
- 对常见质疑的回答（很有说服力的一段）：“没有形式化方法我们不也做出了许多软件？”——“我们做得并不好”；“没学建筑也能搭窝棚，但能让他设计摩天楼吗？”
- 坦承局限：非形式需求到形式规范的关系不可能形式化处理；规范可读性差；证明需要强工具；不能保证不出错，只是有所帮助。安全攸关（safety-critical）/生命攸关（life-critical）系统（核电监控、铁路信号、医疗设备）是刚需场景。
第 2 讲：基本数学描述工具
Z 的数学基础：命题逻辑与谓词逻辑、等词、集合、关系、函数、序列。给出了 Z 与朴素描述对比的写法约定（如集合 ∈、关系像、函数映射等记号体系）。这是 Z 规范的全部”词汇表”。
第 3 讲：模式（Scheme / Schema）
- 动机：纯数学语言没有结构，稍复杂就不可读。模式为描述增加结构：把描述组织成命名的小块，提供封装与重用。
- 模式即”声明 + 谓词”的封装：可作为类型、声明、谓词三种方式使用；支持重命名、修饰（hide/rename）和模式演算（合取、包含等），是 Z 区别于纯数学记法的核心机制。
第 4 讲：证明和推导（150 页，主体讲次）
形式规则、逻辑推理、等式和定义的推理。这是全课程篇幅最大的一讲（约占全部页数 2/3），展开 Z 的推导规则体系——规范不是写完就完，性质要靠演算证明。
第 5 讲：描述技术
规范的标准结构：非形式说明文字 + 全局常量（公理引入或类型实例化）+ 抽象状态模式（含状态不变式，必须仔细考虑）+ 各操作定义 + 前条件（操作正常应用对状态的要求）+ 非正常行为定义 + 重要性质证明。
- 提升（free/restricted lifting）：用函数索引数据类型，为大系统构造分层规范。
- 计算与简化技巧：操作定义应可机械化简化。
第 6 讲：数据精化
- 精化 = 去除规范中的非确定性、做出设计决策，使规范一步步接近可执行代码；定义为抽象数据类型之间的部分序关系（B 精化 A：凡 A 能参与的交互，B 都可代替）。
- 核心概念：模拟（simulation）、向前模拟（forward simulation）与向后模拟（backward simulation）、提取关系（extraction relation）、数据精化。
第 7 讲：精化演算
- 提取函数：若提取关系是全函数（函数式精化），前向模拟证明义务可大幅简化——实践中几乎总是如此。
- 数据精化的计算：给定全且满的提取函数 f，可直接计算出最弱精化（抽象操作 → 具体操作的等式），而非盲目猜测再验证。
- 经典例子：温度传感器——抽象层用华氏温度（绝对 0 度到 5000 度），实现层改用摄氏，通过全双射提取函数机械导出具体初始化与增减操作。
- 提升的精化：提升对精化具有单调性——提升的精化 = 精化的提升，故可独立精化分层的某一层而不影响系统其他部分。
实例研究：X 光治疗仪实时内核（large-example1）
嵌入式实时内核（后台进程 + 中断处理器 + 优先级调度），原系统约 50 页汇编、目标码近 1K。用 Z 规范分析发现原实现存在死锁：中断全禁止时处理器空等待进程运行；实时并行系统此类错误极难靠测试暴露。原系统靠限时硬件兜底才未危及病人。这是”形式化方法能发现测试发现不了的错误”的实证案例。
可行动点与关联
- 写嵌入式/安全攸关需求时，借鉴第 5 讲的规范结构（状态不变式 + 前条件显式化）；
- 抽象→实现的数据映射（如单位换算、编码变换）可套用第 7 讲”全双射提取函数 + 最弱精化计算”，直接算出实现层操作而非手写再测；
- 本系列是 2006 年前后 Z/ B 方法教学的代表性中文材料，可与 软件体系结构编档-Lecture-13、软件体系结构描述-Part4-软件架构课程Lecture-7 等田浩然上传的软件工程课程资料互相参照（同期北大/复旦课程资料包）。
来源：阿里云盘 /田浩然上传的资料/形式化方法/（fm01-fm07 + large-example1，共 8 个 PDF，234 页，全部文本型直接提取）。