软件形式化方法-课程讲义全套（王捍贫）

北京大学研究生课程《软件形式化方法》（0C113）的核心讲义，作者王捍贫（Hanpin Wang）。共 6 份 PDF 讲义（另有 overview.ppt 3.22MB 未下载），构成”逻辑 → 建模 → 规约”三段式验证知识体系。与 形式化方法-裘宗燕-课程讲义 互补：那份是概论性质，本套是完整技术教材。

验证三步法（全书主线）

1. Modeling（建模）：把系统表示为迁移系统（transition system）
2. Specifying（规约）：用线性时序逻辑（LTL）写性质
3. Verifying（验证）：检查模型是否满足规约（satisfaction）

关心对象：顺序系统、并发系统（多线程/并行/分布式）、I/O 系统、反应式系统、嵌入式系统。

第一部分：逻辑与定理证明（logic-1 / logic-2 / Logic-3）

命题逻辑

• 语法：Form ::= P | true | false | (form∧form) | (form∨form) | (form→form) | ¬form；优先级 ¬ > ∧ > ∨ > →，∧∨ 左结合
• 语义：赋值 σ: AP→{TRUE,FALSE}，解释函数 Mσ 归纳定义各联结词
• 公式分类：重言式（tautology）/ 可满足（satisfiable）/ 矛盾（contradiction）
• 公理系统：Ax1-Ax3 + MP 规则；前向推理序列定义 Γ⊢α；内定理 ⊢α
• 可靠性（soundness）+ 完全性（completeness）均成立
• 判定性：⊢α 等价于重言式判定，可归约为 SAT——NP 完全问题

一阶逻辑（带等词）

• 语法：签名 <V,F,R>（变量/函数符号/关系符号，均带元数，常量视作 0 元函数）；项 Term ::= var | constant | func(term,…,term)；原子公式 rel(term…) 或 term≡term；加量词 ∀v / ∃v
• 自由/约束变元、替换 φ[e/v]（要求 e 对 v 在 φ 中可自由代入）
• 语义四件套：结构 (D,F,R,I)（非空论域+函数解释+关系解释）、赋值 a:V→D、项解释 Ta、公式解释 Ma；∀ 要求所有 a[d/v] 满足，∃ 只需某个
• 模型概念：若结构 S 上所有赋值满足 φ，称 S 是 φ 的模型（⊨ˢφ）；对所有结构成立即重言式
• 一阶证明系统：命题公理 Ax1-3 + Ax4（∀v(φ→ψ)→(φ→∀vψ)，v 不在 φ 中自由）、Ax5（∀vφ→φ[e/v]）、等词公理 Ax6-8；规则 MP + 概括规则 G
• 一阶逻辑不可判定（重言式问题半可判定）；Hao Wang（王浩）是自动定理证明先驱，归结（resolution）方法

PVS 式序列（sequent）证明系统

• 序列 = (φ1∧…∧φn)→(ψ1∨…∨ψm)，左侧为前件（合取），右侧为后件（析取）；n=0 时约定空合取为 TRUE，故任何公式自身也是序列
• 证明过程：pending 目标列表——用规则把目标约简为更细子目标，或用公理 discharge，直到初始目标消去
• PVS 命令式规则：eliminate / flatten / split / assumption / Skolemize / instantiate / substitution
• 完整实例：证明 ⊢((A→C)∧(B→C))→((A∨B)→C)，先 flatten 拆前后件，split 分情况，最后 eliminate 关闭——展示了交互式定理证明的实际操作手感

第二部分：软件系统建模（Modeling-1 / modeling-2）

迁移系统

• 定义：三元组 (S, S₀, R)，S 状态集、S₀⊆S 初始状态集、R⊆S×S 迁移关系
• 示例：减法实现整数除法（y1 商、y2 余数循环减）逐语句展开状态轨迹
• 逻辑表示法（符号模型检验的基础）：状态=变量赋值；初始条件=无量词一阶公式；迁移=关于 V 与孪生变量集 V’ 的一阶公式（如 x’=(x+y) mod 2 ∧ y’=y）
• 教材定义变体：变量集 V + 状态集 + 迁移集（每个迁移有使能条件 e 和变换 (v1,…,vn):=(e1,…,en)）+ 初始条件 I

数字电路建模

• 模计数器：三触发器 V={v0,v1,v2}，用布尔公式写迁移关系
• 一般方法——同步电路：R(V,V’) ≡ ⋀(vi’ = fi(V))；异步电路：各单触发器更新关系的析取

顺序程序建模（操作语义的迁移系统形式）

• 程序加标号 P^L，引入程序计数器变量 pc（pc=^ 表示未在运行）；入口标号 m、出口标号 m’
• 每条语句的转换关系 C(l, stmt, l’)：
  • 赋值：pc=l ∧ pc’=l’ ∧ v’=e ∧ same(V{v})
  • skip：pc=l ∧ pc’=l’ ∧ same(V)
  • 顺序复合：pc=l∧pc’=l1’∧C(l1,P1,l2’) ∨ pc=l1∧pc’=l2’∧C(l2,P2,l’) 的拼接
  • if/while：按分支条件拆成多公式析取
• 整个系统的转换 = 所有语句转换关系的析取

并发程序建模（交错语义）

• 异步并发 cobegin P1‖…‖Pn coend：任何时刻只有一个进程迁移；每进程独立 pc_i
• 初始状态：pre(V) ∧ pc_i 各自就位
• 共享变量原语：wait(b)（b 假则原地等待）、lock(v)/unlock(v) 各拆两分支
• 经典互斥算法（turn 变量）建模实例：进入区/临界区/退出区的 NC/CR 标号迁移
• 粒度权衡：C 语句 x:=x+y 若拆到汇编级（load/add/store）状态数暴涨且引入假负例（false negative）
• 执行（execution）定义：极大状态序列，逐步启用迁移；有限执行用末尾”stuttering”延为无限
• 关键概念：可达状态、确定性/非确定性、公平性（fairness）、自动建模之难

第三部分：形式规约与 LTL（specification-1）

形式化方法的评价维度

Formal（唯一解释）、Intuitive（易读）、Succinct（规模合理）、Effective（可查无矛盾/可实现/可满足）、Expressive（能生成初始代码）。核心立场：规约描述”实现的性质”而非实现本身。

Kripke 结构

M = (S, S0, R, L)：四元组，R 必须完全（每状态必有后继），L: S→2^AP 给状态打原子命题标签——LTL 语义的载体。

LTL 语法与语义

• 算子：O(next)、、<>(eventually/diamond)、U(until)、R(release)，加命题联结词
• 语义在执行序列及其后缀上归纳定义；P⊨φ 当且仅当 P 的每条执行都满足 φ
• 冗余算子可删：<>p = true U p；[]p = ¬<>¬p；pRq = ¬(¬p U ¬q)
• 惯用组合：[]<>p（无穷多次发生）、<>[]p（最终永远）、([]<>p)→([]<>q)（公平性典型形式）
• 分配律辨析：=[]φ∧[]ψ 成立，但<>(φ∧ψ)≠<>φ∧<>ψ；([]<>φ)∨([]<>ψ)=[]<>(φ∨ψ) 成立，反向不等
• 经典例题：弹簧玩具（release/pull，extended/malfunction 状态）逐序列判定 satisfaction；红绿灯 Green→Yellow→Red 的 LTL 规约——“恰好一灯亮”用 []三互斥∧三析取，“正确变色”用 []( (gr U ye)∧(ye U re)∧(re U gr) )；Green→Yellow→Red→Yellow 变体需按初始灯位分别写 U 链
• 互斥规约示例：[](PC0=NC0 → <>PC0=CR0)（有界等待意向）、[](PC0=NC0 U Turn=0)（等待 turn 归还）
• 程序正确性的 LTL 表达：部分正确性 init∧；终止性 init∧<>finish；全正确性 init∧<>(finish∧ψ)；不变式 init∧[]φ
• LTL 证明系统：¬<>p↔[]¬p + 命题公理 + →([]p→[]q) + 归纳规则 + (pUq)↔(q∨(p∧O(pUq))) 等展开公理

可行动点与工程关联

• LTL 规约模板可直接用于多线程代码审查：把锁/临界区标注成原子命题，即可写互斥与无死锁性质
• 顺序程序→迁移系统的 pc 编码法，就是模型检验工具（SPIN 等）翻译程序源码的底层原理
• PVS/sequent 风格与 Isabelle/Coq 交互式证明一脉相承：flatten/split/instantiate 概念可平移
• 交错语义 vs 粒度权衡，对应今天并发测试的 state-space explosion 问题

关联

• 形式化方法-裘宗燕-课程讲义 — 同课程主题的概论版（Z 语言向）
• 云盘同目录另有 overview.ppt（3.22MB）为课程总览，未消化