企业官网建设流程全解析

两年前我第一次接触操作系统形式化验证时，导师递给我一个任务：验证一个迷你调度器的就绪队列性质。我当时的反应和大多数人一样——队列不就是个列表嘛，往里塞任务再取出来，这个有什么好证的？结果真上手才发现，光是把“加入任务后再拿出任务，队列能恢复原样”写成定理，就够我折腾大半天。问题全出在列表和集合这些最底层的数据结构上：递归归纳的边界、空与非空的分支、去重与顺序之间的微妙关系，每一条都在考验你对逻辑表达式的掌控力。这个系列的第二篇，我决定把HOL列表与集合的玩法从头到尾认真捋一遍，把我踩过的坑、验证过的套路和可直接照抄的证明模式都放出来。无论你是正在学HOL4的学生，还是想给系统代码加一层形式化保障的工程师，这篇文章都能帮你少走弯路。

1. 为什么操作系统验证绕不开列表和集合

1.1 从“就绪队列验证”这个需求说起

说到操作系统内核里的数据结构，列表和集合几乎无处不在。就绪队列是列表，进程集合是集合，页框分配状态是集合，设备链表是列表，打开文件表可能是列表加集合的组合。形式化验证要做的第一步，就是把运行时的数据结构“翻译”成定理证明器里的逻辑对象，然后对这个对象证明不变量。

以就绪队列为例。一个最朴素的需求是：把一个进程加入就绪队列，它就应该出现在队列的末尾；把它从队首取出来调度，其余进程的相对顺序不能变。用HOL的列表建模时，“进程在队列里”这个命题天然对应列表的成员关系，而“调度后队列恢复现场”则对应列表在入队和出队操作下的等式关系。这种建模方式直接、自然，但真正动手证明时你会发现，列表的每个操作都对应一堆归纳情况和case分析，普通程序里一个循环就搞定的事，在定理证明器里可能要拆分出三四个子目标。

集合在操作系统验证中的角色同样关键。比如页框分配器要维护“已分配页框集合”和“空闲页框集合”，这两者必须是不相交的，且它们的并集等于全部可用页框。如果你用列表模拟集合，就得额外处理重复元素和顺序问题，白白增加证明负担。HOL里集合的本质是谓词，x IN s本质上就是s x，集合的运算也被翻译成逻辑连接词。这个设计让“两个集合相等”变成了“两个谓词等价”，证起来比列表的等式更干净。

所以结论很直接：列表负责“有顺序的排列”，集合负责“无顺序的归属”。操作系统里两类需求都有，两种数据结构都要会。这就是这个系列教程选了HOL列表与集合作为第二篇的原因。

1.2 HOL里的列表和集合与普通语言有什么不同

第一次用HOL的人特别容易栽在一个思维惯性上：把普通编程语言里的“列表”和“集合”概念原封不动搬进来。这在思想的起点上就走偏了。

普通语言里，列表就是一个运行时数据结构，你关心的是它的内存布局和操作复杂度。HOL里的列表是一种归纳定义的代数数据类型，你的任务不是“调用它的方法”，而是“证明它的性质”。普通语言里，集合通常是一个哈希表或者树，你关心的是插入和查找的速度。HOL里的集合是逻辑谓词，你操作的是逻辑蕴含、合取、析取。换句话说，HOL列表与集合不是给你“用的工具”，而是给你“证明的对象”。

这种差异最直接的影响体现在证明风格上。普通代码出bug你会调试、打日志、看堆栈；HOL证明出问题你会展开定义、选择归纳变量、构造存在性实例，然后看着子目标一层层化简。刚开始可能很不习惯，但你适应了之后会发现，恰恰是这种“一切都可展开、一切都可检查”的机制，给了你在普通测试里拿不到的信心——当一条定理在HOL4里证明通过，它就不只是在几个测试用例上成立，而是在所有可能的输入上都成立。

2. HOL中列表的定义与常用武器

2.1 列表的递归构造：Nil 与 Cons

HOL里列表的定义非常经典，本质就是两个构造子的递归数据类型：

datatype 'a list = [] | :: ('a, 'a list)

注意这里的[]是空列表构造子，::是中缀形式的“头部加尾部”构造子。[1;2;3]实际上就是1 :: 2 :: 3 :: []的语法糖。我刚开始用的时候总觉得这个定义简单到不值得关注，但后来才意识到，这个递归结构是列表所有性质的根源。

因为列表是递归定义的，你定义在列表上的函数几乎全都是递归函数。比如求长度LENGTH：

(LENGTH [] = 0) ∧ (LENGTH (h :: t) = 1 + LENGTH t)

比如拼接APPEND（HOL里也写作++）：

(APPEND [] l = l) ∧ (APPEND (h :: t) l = h :: APPEND t l)

这些定义遵循同一种模式：先给空列表的情况，再给非空列表的情况，而非空情况中递归调用作用在尾部t上。只要你能写出这种递归定义，HOL就会自动为你生成对应的归纳定理，这就是我接下来要说的核心武器。

2.2 必背的高频列表定理

用HOL证明关于列表的性质，绕不开下面这几个定理。我把它们整理成一张表，按频率从高到低排列，每个都标注了典型使用场景：

这几个定理不是我瞎列的，而是我在证明调度器、文件系统元数据时反复用到的“基础弹药”。它们的共同特点是：把复杂操作拆成简单操作的组合，把关于结构的情报转化为关于逻辑的情报。

特别提一下MEM——它表示“元素出现在列表中”。在操作系统的场景里，x MEM run_queue可以读作“进程x在就绪队列中”，这个命题再配合列表操作，就能描述几乎所有队列不变量的基础形式。

2.3 列表归纳法实操：证明 LENGTH_APPEND

理论说再多，不如实际手推一遍。我现在带你亲手证明LENGTH_APPEND，这是列表证明的“Hello World”，但里面包含的技法可以复用到大多数场景。

要证的定理是：

∀ l1 l2. LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2

第一次看到这个定理，很容易想当然地对l2做归纳，或者对两个参数同时归纳。正确做法是对l1归纳，因为APPEND的递归定义是围绕第一个参数展开的。方法如下：

第一步，对l1使用LIST_INDUCT，归纳会分成两个子目标。空列表子目标：

LENGTH (APPEND [] l2) = LENGTH [] + LENGTH l2

用APPEND的定义直接把左边化成LENGTH l2，再用LENGTH的空列表定义把右边的LENGTH []化成0，最后用算术化简收掉。这里我习惯用simp [APPEND, LENGTH]一条命令搞定，但新手建议先用rewrite或fs逐条展开，看清每一步发生了什么。

非空列表子目标是整个证明的关键：

LENGTH t + 1 + ? （假设 LENGTH (APPEND t l2) = LENGTH t + LENGTH l2）

具体展开后，左边会用APPEND的h::t分支变成LENGTH (h :: APPEND t l2)，再用LENGTH的定义变成1 + LENGTH (APPEND t l2)。此时必须代入归纳假设LENGTH (APPEND t l2) = LENGTH t + LENGTH l2，右边LENGTH (h::t) + LENGTH l2变成1 + LENGTH t + LENGTH l2。两边一化简，等式平凡成立。

这里有个很多新手栽过的坑：如果你对l2做归纳，APPEND的定义不会自动拆开第一个参数的 head 和 tail，整个证明会卡死在“APPEND t l2”这种无法化简的形式上。所以记住一条经验：归纳变量必须选递归定义中参与递归的那个参数。

3. HOL中的集合：本质与推理套路

3.1 集合的本质是谓词

HOL里的集合，本质上就是一个返回布尔值的函数。s是一个集合，x IN s在底层就是s x。整个集合理论建立在这个简单的洞察上：一个集合就是描述“哪些元素属于它”的谓词。

这个设计带来两个直接好处。第一，集合的运算可以直接用逻辑连接词定义。比如并集：

s1 ∪ s2 = λx. x IN s1 ∨ x IN s2

交集：

s1 ∩ s2 = λx. x IN s1 ∧ x IN s2

第二，证明集合相等，用的不再是“两个容器内容一样”这种运行时直觉，而是外延性公理：两个集合相等，当且仅当它们的每一个元素归属都等价。换句话说，你要证s1 = s2，只需证∀x. x IN s1 ⇔ x IN s2。这个套路在HOL中有一个专门的引理，我用SET_EQ或者EXTENSION来触发它。

3.2 常用集合运算与推理套路

集合推理在HOL里很少需要你从零开始，大部分工作就是“展开定义再加上逻辑推理”。我按使用频率整理一下常用武器：

• UNION_COMM / UNION_ASSOC：并集的交换律和结合律，在处理多个集合合并时是主力。
• INTER_COMM / INTER_ASSOC：交集的交换律和结合律。
• SUBSET_ANTISYM：两个方向都有子集关系，就得到集合相等，是证明集合相等的常规路线。
• IN_UNION：x IN s1 ∪ s2 ⇔ x IN s1 ∨ x IN s2，遇到member命题第一时间展开它。
• DELETE_INSERT、INSERT_DELETE：集合的插入和删除操作之间的关系，在建模页框分配这类场景时特别常用。

实际证明中的套路一般是：先做集合外延展开，得到∀x. x IN A ⇔ x IN B；然后用EQ_TAC把双向蕴含拆成两个方向；每个方向再根据具体的IN定义做逻辑推理。

以并集结合律为例，证明s1 ∪ (s2 ∪ s3) = (s1 ∪ s2) ∪ s3时，外延展开之后你面对的是纯命题逻辑的等价式子。这种证明完全可以用metis_tac或者其他自动化策略暴力收官，但为了锻炼手感，我建议新手手动走一遍：先展开三次IN_UNION，把IN的析取结构全部暴露出来，再用命题逻辑的结合律合并。手工走通之后，你会发现集合证明的套路就这么简单——集合运算是壳，逻辑运算才是核。

3.3 FINITE 与无穷集合的边界

集合推理里有一个操作系统验证绕不开的概念：有限性。因为内核里的集合几乎都是有限集合，而很多证明技巧需要“集合有限”作为前提。

HOL对FINITE的定义是归纳式的：空集有限，往有限集里插入一个新元素得到的集合仍然有限。这条定义链得到了一个重要结论：任何有限集都可以被转换成一个列表。实际使用中，FINITE_LIST_TO_SET保证任何列表转成的集合都有限；反过来，SET_TO_LIST可以从有限集中构造出一个列表。

我做文件系统链接计数验证时，就吃过“忘记证明有限性”的亏。当时想对一个已分配页框集合做遍历求和，直接调用一个依赖列表表示的工具函数，结果证明卡住。后来才发现，那个工具函数的前提条件里要求集合必须是FINITE的，而我完全没提供这个前提。从那以后我养成了一个习惯：建模阶段就提前确认每个集合操作的有限性要求，能证明的在定义时就当附带给出来。

4. 列表与集合联合作战：一个系统验证小案例

4.1 建模：模拟调度器与页框分配集合

前面铺了这么多，现在来看一个综合案例。我基于模拟项目X做了一套极简内核模型，核心是两个部分：就绪队列用列表建模，已分配页框用集合建模。

先看数据结构定义：

(* 就绪队列：进程ID列表 *) Definition run_queue_def: run_queue = [] : num list End (* 入队：把任务追加到队尾 *) Definition enqueue_def: enqueue q task = APPEND q [task] End (* 出队：取队首，返回原队列去掉队首 *) Definition dequeue_def: dequeue [] = NONE ∧ dequeue (h::t) = SOME (h, t) End (* 从队列提取进程集合 *) Definition process_set_def: process_set q = LIST_TO_SET q End (* 已分配页框集合 *) Definition alloc_def: allocated_frames : num set = {} End

注意process_set_def这一条，它把列表和集合连接了起来。LIST_TO_SET会把列表里的元素收集成集合，自动去重。这正是操作系统场景所需要的：队列里进程出现两次可能是个bug，但集合视角下你关心的只是“这个进程是否在某处存在”。

4.2 验证“入队后进程集合恰好扩张一个元素”

我要验证的第一个核心性质是：把一个进程加入就绪队列后，进程集合等于原集合与“新进程”的并集。定理陈述如下：

∀q task. process_set (enqueue q task) = process_set q ∪ {task}

这个定理听起来很直观，但证明过程能体现列表和集合配合的标准套路。我用rw [enqueue_def, process_set_def]把定义全部展开，目标变成：

LIST_TO_SET (APPEND q [task]) = LIST_TO_SET q ∪ {task}

接着调用列表与集合互转的核心引理LIST_TO_SET_APPEND：

LIST_TO_SET (APPEND q [task]) = LIST_TO_SET q ∪ LIST_TO_SET [task]

右边化为LIST_TO_SET q ∪ {task}，正好为目标。整个证明最微妙的地方在于LIST_TO_SET的去重行为：如果task已经在q里，左边的集合并不会多出一个元素，右边的并集同样不会多出元素。这个“去重一致性”在逻辑上自动成立，不需要单独证明。我第一次推到这里还有点半信半疑，后来专门验证了一遍task已在列表中的情况，确认两边的确都等于原集合，这才放心。

第二个要验证的性质跟出队相关：出队不会把任何进程从集合中凭空变出来。具体来说，如果dequeue q = SOME (h, t)，那么process_set t ⊆ process_set q。这个定理的价值在于，它保证了调度器取出队首后，剩下的进程仍然属于原有进程集合，不会出现“进程消失”这种不变量破坏。证明方法是对q做Cases_on分空和非空两种情况，然后展开dequeue_def和process_set_def，用列表的MEM与集合归属的转换关系收尾。

4.3 这个案例对操作系统验证的扩展思路

我在模拟项目X里验证完这两个性质后，最大的感受是：列表与集合的组合是系统验证的基本功，它们能覆盖的远不止调度器。你可以把run_queue换成“打开文件表”，把process_set换成“已打开文件描述符集合”，模式完全一样。

更关键的是，这套建模思路可以往上叠加不变量。比如“所有在就绪队列里的进程都处于就绪状态”，这需要集合ready_state_set与process_set q的子集关系；比如“已分配页框集合与空闲页框集合互不相交”，这需要交集为空的集合论证。而这些不变量，最后都会化约为本文前面讲的列表和集合的基础定理。基础不牢，上层根本走不动。

5. 常见问题与排查实录

5.1 最常翻车的五个点

我在HOL列表与集合的实践中，见过太多人（包括我自己）反复踩同样几个坑。这里挑五个最典型的，每一个都附上现场描述和解决思路。

第一个坑：归纳变量选错。证明关于APPEND的性质时选了第二个列表做归纳，导致递归定义无法展开，整个证明卡死在原地。解决方法前面说过，观察递归定义里哪个参数在递归，就选哪个参数做归纳。还有个通用判断标准：如果归纳到一半发现子目标里的结构无法用定义化简，多半是归纳变量选错了。

第二个坑：集合外延展开后方向搞反。用SET_EQ展开集合相等后，两个方向的蕴含有时会让人觉得两边长得一样，但如果你在展开之前没有正确定义集合运算的优先级，很容易出现x ∈ A ∨ x ∈ B和x ∈ B ∨ x ∈ A这种表面上看起来不同、实际上等价的式子。解决方法是先fs []把集合运算全部展开成逻辑公式，再用taut_tac或者prove_tac做纯命题逻辑的收尾。

第三个坑：FULL_SIMP_TAC把公式炸了。有些集合定义展开后会产生大量连接词，如果直接full_simp_tac，轻则目标变成一坨不可读的命题逻辑公式，重则证明器内存暴涨。我的习惯是分步化简：先用simp []只展开必要的定义，再用较小的规则集合做定点化简，最后才考虑用全量简化。

第四个坑：EXISTS_TAC找错存在性实例。集合证明里经常需要“构造一个元素证明属于某个集合”，这时如果选错了 witness，后续子目标可能根本走不通。比如证明∃x. x ∈ s，直接挑s里的任意元素不一定行，因为你还得先证明它有某个性质。实践经验是，在选 witness 之前先把目标化简到最简形式，看清到底需要什么类型的元素。

第五个坑：忽略有限性前提。前面已经讲过，当目标要求遍历集合时，哪怕只差一个FINITE s前提，证明也会卡住。我现在的做法是在建模阶段就给每个集合加上有限性引理，并尽量把“有限性”放进不变量里一起证明。

5.2 调试技巧速查

HOL列表与集合的调试，核心是“看清楚证明器在做的事”。我给你几个亲测有效的速查技巧：

另外一个我特别想分享的心得：HOL4的证明脚本不要一次性写很长。我用g开目标，用e逐条执行策略，每执行完一步就停下来看看当前目标变成了什么。这样虽然看起来慢，但能防止大方向走偏后整个脚本全部报废。等到每一步都确认无误，再把这些e串成完整的prove或store_thm，效率反而高出一大截。

调试时还有一个容易被忽略的工具：类型打印。如果目标里出现大幅变量，分不清哪个是列表的h、哪个是集合的s，可以在脚本开头开启类型显示，让所有变量带上类型注解。这个习惯帮我省了不少脑力。

最后分享一个小技巧：证明列表与集合结合的性质时，提前把LIST_TO_SET_APPEND、MEM_LIST_TO_SET这类桥梁引理准备好。它们会在证明中反复出现，与其每次都现场展开一遍，不如先作为本地引理prove好放一边，后面用fs一个接一个用。我在模拟项目X里，几乎每三个证明就会用到一次这类桥梁引理。现在一看到LIST_TO_SET出现在目标里，我第一反应不是展开它，而是搜索有没有现成的互转定理可以直接用。这个思路的转变，是HOL列表与集合从入门到上手的真正的分水岭。