1. 为什么程序验证绕不开一阶逻辑很多人第一次接触程序验证脑子里冒出来的第一个疑问就是我写代码写得好好的为什么非要学一阶逻辑这玩意儿看起来像是数学系的东西跟工程实践有什么关系我当初也是这么想的直到真正动手做验证工具的时候才发现一阶逻辑不是选修课而是必修课而且是那种你绕不过去的必修课。程序验证的本质是什么说白了就是用数学手段证明程序的行为符合预期。你要证明的东西最终都要表达成某种逻辑公式。命题逻辑表达能力太弱连对于所有自然数n数组前n个元素都是有序的这种话都说不出来。而一阶逻辑引入了量词和谓词刚好能把程序中最常见的性质——循环不变式、数组边界、链表完整性——精确地形式化。这篇文章主要面向三类人一是正在学习程序验证但被逻辑符号劝退的开发者二是想自己动手写验证工具、但不确定底层逻辑该怎么落地的工程师三是已经用过一些验证工具但对其内部原理一知半解的进阶用户。我会从一阶逻辑的语法和语义讲起然后重点讲它在程序验证中到底怎么用最后给出一个可以实际跑起来的验证流程。整个过程我会尽量用代码和具体例子说话少堆公式。需要提前说明的是一阶逻辑本身是一个很大的话题完整展开可以写一本书。我这里聚焦的是程序验证场景下最需要掌握的那部分包括语法构造、语义解释、量词处理、以及和程序语义的对应关系。那些偏纯数学的模型论内容我会点到为止不会深挖。2. 一阶逻辑的语法骨架从符号到公式2.1 一阶逻辑到底比命题逻辑多了什么命题逻辑的最小单位是原子命题比如P、Q、R它只关心真假组合不关心命题内部结构。这就导致一个问题你没法表达x大于0和y大于0之间的共同结构只能把它们当成两个无关的原子命题。一阶逻辑把原子命题拆开了引入了项和谓词的概念。项可以理解为指代对象的表达式它由变量、常量和函数符号组成。比如x、0、f(x, y)都是项。谓词则是关于对象的断言比如Greater(x, 0)表示x大于0。这样一来所有自然数都大于等于0就可以写成∀x. (Nat(x) → GreaterEq(x, 0))表达能力比命题逻辑强了不止一个量级。这个区别在程序验证里非常关键。程序里到处都是对于所有数组下标i、存在一个返回值r这样的描述命题逻辑根本无能为力一阶逻辑才能精确刻画。2.2 项、谓词、量词三个核心构件一阶逻辑的语法可以拆成三层。最底层是项它描述对象中间层是原子公式它描述关于对象的断言最上层是公式通过逻辑连接词和量词把原子公式组合起来。项的定义是递归的变量是项常量是项如果f是n元函数符号t1到tn是项那么f(t1,...,tn)也是项。注意函数符号和谓词符号的区别——函数返回对象谓词返回真假。这个区分在实现验证工具时非常重要因为类型检查必须严格区分这两类符号。原子公式的形式是P(t1,...,tn)其中P是n元谓词符号。公式则通过以下规则构造原子公式是公式如果φ是公式那么¬φ是公式如果φ和ψ是公式那么φ∧ψ、φ∨ψ、φ→ψ、φ↔ψ都是公式如果φ是公式x是变量那么∀x.φ和∃x.φ都是公式。这里有个容易踩的坑量词的辖域。∀x. P(x) ∧ Q(x)和(∀x. P(x)) ∧ Q(x)是完全不同的两个公式。前者中Q(x)里的x是被量词约束的后者中Q(x)里的x是自由的。我在早期实现解析器的时候就因为没处理好辖域导致生成的公式语义完全错了排查了大半天才发现是括号的问题。2.3 自由变量与约束变量一个必须搞清楚的区别自由变量和约束变量的区分是一阶逻辑里最基础但也最容易出错的地方。一个变量在公式中是约束的如果它出现在某个量词的辖域内否则它是自由的。比如在∀x. (P(x) ∧ Q(y))中x是约束变量y是自由变量。这个区分为什么重要因为一个公式的语义依赖于自由变量的赋值。P(y)本身没有真假只有给y赋了具体值之后才有真假。而∀x. P(x)是一个封闭公式它本身就有确定的真假。在程序验证中自由变量通常对应程序的状态变量约束变量则是临时引入的。比如验证循环的时候我们可能会写∀i. (0 ≤ i n → a[i] ≤ a[i1])这里的i是约束变量n和a是自由变量对应程序中的数组长度和数组本身。提示实现验证工具时替换操作必须小心变量捕获。把∀y. P(x, y)中的x替换成y如果直接替换会得到∀y. P(y, y)这就把原本自由的y给捕获了。正确的做法是先对约束变量重命名比如改成∀z. P(y, z)。3. 语义解释公式什么时候为真3.1 结构和赋值给符号赋予意义语法只管符号怎么排列语义才管符号是什么意思。一阶逻辑的语义建立在一个结构也叫解释之上。一个结构包含一个非空的对象集合论域、为每个常量符号指定一个论域中的元素、为每个函数符号指定一个函数、为每个谓词符号指定一个关系。举个例子假设论域是自然数集合常量符号0解释为数字0函数符号解释为加法谓词符号解释为小于关系。在这个结构下公式∀x. ∃y. (x y)就是真的因为对任何自然数都能找到一个更大的自然数。但如果论域换成有限集合这个公式就可能为假。赋值则是给自由变量指定论域中的元素。一个公式在某个结构和某个赋值下为真记作M, σ ⊨ φ。这个符号读作结构M和赋值σ满足φ。3.2 满足关系的递归定义满足关系的定义是递归的跟语法的构造规则一一对应。原子公式P(t1,...,tn)在M和σ下为真当且仅当t1到tn在M和σ下的值构成的有序元组属于P在M中的解释。连接词的满足关系就是标准的真值表。量词的处理稍微复杂一点∀x.φ为真当且仅当对论域中所有元素dφ在把x赋值为d的赋值下都为真。这个递归定义看起来简单但它是所有自动验证工具的理论基础。SAT求解器、SMT求解器、定理证明器本质上都在做同一件事判断某个公式在某个理论结构下是否可满足。3.3 有效式、可满足式与不可满足式在程序验证中我们最关心的是公式的可满足性。一个公式是可满足的如果存在某个结构和赋值使它为真是不可满足的如果对所有结构和赋值都为假是有效的如果对所有结构和赋值都为真。这三者的关系可以用否定来串联φ是有效的当且仅当¬φ是不可满足的。这个等价关系是自动验证的核心——要证明程序满足某个性质φ我们通常转化为证明¬φ不可满足。实际工具里SMT求解器接收一个公式返回sat或unsat。如果返回unsat说明否定不可满足原性质成立。如果返回sat求解器还会给出一个模型这个模型往往对应一个反例——程序在某种输入下违反了性质。这个反例对调试非常有用我后面会详细讲怎么利用它。4. 一阶逻辑怎么描述程序从代码到公式4.1 霍尔三元组与一阶逻辑的对应程序验证里最经典的框架是霍尔逻辑它的核心是霍尔三元组{P} C {Q}意思是如果前置条件P成立执行程序C之后后置条件Q一定成立。P和Q都是逻辑公式通常用一阶逻辑表达。比如一段交换两个变量的代码前置条件是x a ∧ y b后置条件是x b ∧ y a。这里的等号是谓词a和b是自由变量代表初始值。整个三元组表达的就是交换操作的正确性。霍尔逻辑的推理规则本质上是在一阶逻辑里做推导。赋值公理、顺序规则、条件规则、循环规则每一条都可以看作一阶逻辑的推理模式。理解这一点之后你会发现程序验证工具做的事情其实就是把程序翻译成一阶逻辑公式然后交给求解器判断。4.2 循环不变式一阶逻辑最典型的应用场景循环是程序验证里最难处理的结构因为它可能执行任意多次。霍尔逻辑用循环不变式来处理找一个断言I使得I在循环开始前成立且每次循环体执行后I仍然成立那么循环结束后I依然成立。用一阶逻辑写出来就是{I ∧ B} C {I}其中B是循环条件C是循环体。这个不变式I必须用一阶逻辑表达而且必须足够强强到能推出我们想要的后置条件。举个具体例子验证一个数组求和循环。循环不变式可能是sum Σ(k0..i-1) a[k] ∧ 0 ≤ i ≤ n。这里的求和符号在纯一阶逻辑里其实不能直接写需要展开成递归定义或者用辅助函数。这是实际验证中经常遇到的麻烦——一阶逻辑的表达能力有边界有些性质需要扩展才能写出来。注意循环不变式的构造是程序验证中最需要人工介入的环节。自动工具可以验证不变式是否正确但找到一个合适的不变式往往需要人的洞察。我个人的经验是先写出循环的意图然后把它和循环变量的范围结合起来通常能得到一个可用的不变式。4.3 数组、指针和堆一阶逻辑的扩展需求纯一阶逻辑处理数组和指针会比较吃力。数组本质上是函数从下标到值。a[i]可以看作函数应用a(i)。但数组还有长度、边界这些性质需要额外的谓词来表达。指针和堆更麻烦因为涉及别名和内存布局。实际工具通常会在一阶逻辑基础上扩展引入理论谓词比如数组理论、位向量理论、指针理论。这些理论加上一阶逻辑就构成了SMT-LIB标准里的各种理论组合。我在实现一个简单的验证器时最初想用纯一阶逻辑处理数组结果发现连数组前n个元素有序这种性质都写得很别扭。后来引入了数组理论的select和store操作表达起来就自然多了。这个经验告诉我选对理论比硬用一阶逻辑重要得多。5. 量词实例化自动验证的核心难题5.1 为什么量词让自动求解变得困难一阶逻辑的可满足性问题是半可判定的意思是如果公式不可满足存在算法能在有限时间内证明但如果公式可满足算法可能永远跑不完。这个半可判定性的根源就在量词。无量词的公式命题逻辑层面可以用SAT求解器高效处理。但一旦引入∀和∃求解器就需要在无限多的实例中搜索。∀x. P(x)要检查论域中每个元素如果论域是无限的这就没法穷举。实际工具的策略是量词实例化把量词替换成有限个具体实例然后交给无量词的求解器。比如∀x. P(x)可能被实例化为P(t1) ∧ P(t2) ∧ ... ∧ P(tk)其中t1到tk是当前上下文中出现的项。这个策略不完整——可能漏掉关键实例——但在很多实际场景下够用。5.2 触发器和模式控制实例化的方向SMT求解器处理量词时通常用触发器trigger来控制实例化。触发器是公式中的一个模式当求解器在上下文中找到匹配这个模式的项时就触发一次实例化。比如公式∀x. (f(x) 0 → g(x) 0)如果指定触发器为f(x)那么每当上下文中出现f(a)这样的项求解器就会实例化出f(a) 0 → g(a) 0。触发器的选择直接影响求解效率和成功率。我踩过的一个坑是触发器选得太宽泛导致实例化爆炸求解器跑了几分钟还没结果触发器选得太窄又漏掉了必要的实例导致返回sat但实际上是unsat。后来我的经验是优先选择包含函数符号的模式避免选择纯变量模式因为纯变量模式几乎会匹配所有项。5.3 实例化策略的取舍完整性 vs 效率量词实例化的核心矛盾是完整性和效率。完整的实例化策略比如枚举所有可能的项组合理论上能保证正确性但实际跑不动。高效的策略比如只实例化触发器匹配的项跑得快但可能不完整。实际工具通常采用折中方案先用高效策略跑一遍如果返回unsat就接受结果如果返回sat再用更完整的策略验证这个sat是否真的成立。有些工具还会限制实例化的深度和数量超过阈值就放弃。这个取舍在工程上很重要。我在做验证工具的时候最初追求完整性结果大部分查询都超时。后来改成先快后慢的策略90%的查询能在几秒内出结果剩下的10%再慢慢磨。这个策略在实际使用中体验好很多。6. 动手实现一个迷你验证器6.1 整体架构设计说了这么多理论不如动手写一个。我设计了一个迷你验证器整体架构分四层解析层负责把程序和一阶逻辑公式解析成抽象语法树翻译层把程序语句翻译成霍尔三元组验证条件生成层把三元组转换成纯逻辑公式求解层调用SMT求解器判断公式可满足性。这个架构跟工业级工具比如Boogie、Why3的思路是一致的只是规模小很多。麻雀虽小五脏俱全理解了这个小工具再看大工具就不会觉得神秘。解析层我用Python的lark库写语法翻译层和验证条件生成层是纯Python逻辑求解层调用z3-solver。选择z3是因为它的Python绑定很成熟文档也全适合快速原型。6.2 核心代码从霍尔三元组到SMT查询验证条件的生成是核心。对于赋值语句x : e前置条件P后置条件Q生成的验证条件是P → Q[x/e]其中Q[x/e]表示把Q中的x替换成e。这个替换必须小心变量捕获前面提过。对于顺序组合C1; C2先生成C1的验证条件再生成C2的然后组合。对于条件语句if B then C1 else C2生成两个验证条件分别对应两个分支。对于循环while B do C需要用户提供不变式I然后生成三个验证条件进入循环时I成立、循环体中I保持、循环结束后I ∧ ¬B成立。def vc_assign(pre, post, var, expr): # 生成赋值语句的验证条件: pre - post[var/expr] substituted substitute(post, var, expr) return Implies(pre, substituted) def vc_seq(pre, stmts, post): # 顺序组合从后往前生成 current_post post for stmt in reversed(stmts): current_post vc_stmt(pre, stmt, current_post) return current_post这段代码看起来简单但替换函数substitute的实现很讲究。必须遍历公式的抽象语法树遇到量词时检查变量是否被捕获必要时重命名约束变量。我第一版实现没做重命名结果在测试一个嵌套量词的例子时出了错排查了很久。6.3 实测验证一个数组求和程序我写了一个简单的数组求和程序来测试验证器i : 0; sum : 0; while i n do sum : sum a[i]; i : i 1 end前置条件是n ≥ 0后置条件是sum Σ(k0..n-1) a[k]。循环不变式我设为sum Σ(k0..i-1) a[k] ∧ 0 ≤ i ≤ n。验证器生成的验证条件交给z3求解返回unsat说明程序满足后置条件。整个过程大概两秒钟其中大部分时间花在解析和翻译上求解本身很快。如果我把后置条件改成sum Σ(k0..n) a[k]求解器返回sat并给出一个反例n0时sum0但Σ(k0..0) a[k] a[0]两者不等。这个反例精确地指出了后置条件的错误比人工调试高效多了。提示反例的解读需要一点技巧。z3返回的模型可能包含一些辅助变量的赋值这些变量是翻译过程中引入的不是程序本身的变量。看反例的时候要过滤掉这些辅助变量只看程序变量和输入变量。7. 实际使用中的坑与经验7.1 量词实例化不收敛怎么办量词实例化不收敛是最常见的问题。表现是求解器跑很久不出结果或者内存暴涨。我遇到过的原因主要有三个触发器设计不当、公式结构导致实例化爆炸、以及理论组合引入的额外量词。触发器设计不当是最常见的。比如公式∀x. (P(x) → Q(x))如果没指定触发器求解器可能选P(x)也可能选Q(x)。选P(x)通常更好因为P(x)在上下文中出现的频率可能更低实例化次数更少。我的经验是手动指定触发器并且优先选择出现频率低的谓词。公式结构导致的爆炸通常是因为量词嵌套太深。∀x. ∃y. ∀z. ...这种结构实例化的时候会产生组合爆炸。解决办法是尽量把量词提到最外层或者用Skolem化消去存在量词。Skolem化是把∀x. ∃y. P(x, y)变成∀x. P(x, f(x))其中f是新的函数符号。这样存在量词就没了实例化压力小很多。7.2 循环不变式写不出来的应对策略循环不变式写不出来是程序验证中最让人头疼的问题。自动工具可以验证不变式但生成不变式往往需要人的洞察。我总结了几条实用策略。第一条是从后往前推。先看循环结束后需要什么性质然后反推循环过程中需要保持什么。比如要证明循环结束后sum Σ(k0..n-1) a[k]那么循环过程中sum应该等于已经累加的部分也就是Σ(k0..i-1) a[k]。第二条是加强不变式。有时候一个不变式不够强推不出后置条件需要加上额外的约束。比如加上0 ≤ i ≤ n这样的边界条件。加强不变式不会破坏正确性只会让验证条件更容易证明。第三条是用工具辅助。有些工具能从程序自动推导不变式比如基于抽象解释的工具。虽然推导出的不变式可能不够精确但可以作为一个起点人工再调整。7.3 反例看不懂怎么排查反例看不懂通常是因为翻译过程中引入了太多辅助变量或者反例涉及的输入太复杂。我的排查步骤是这样的先看反例中程序变量的值理解程序在什么输入下违反了性质然后看辅助变量的值理解翻译过程中哪一步出了问题最后简化输入构造一个最小的反例。有一次我验证一个链表操作反例显示某个指针指向了非法地址。我一开始以为是链表操作的问题后来发现是翻译层在处理指针别名时出了错把两个不同的指针当成了同一个。这个bug在正常测试中很难发现因为需要特定的别名关系才能触发。反例帮我精确定位了问题。8. 一阶逻辑在验证工具中的边界一阶逻辑虽然强大但不是万能的。它的表达能力有边界有些程序性质写不出来或者写出来之后求解器处理不了。理解这些边界对选择合适的验证策略很重要。第一个边界是归纳性质。一阶逻辑不能直接表达对于所有自然数nP(n)成立这种归纳性质因为自然数的归纳定义需要二阶逻辑。实际工具通常用递归函数或者归纳数据类型来间接表达但这就引入了额外的复杂性。第二个边界是高阶性质。一阶逻辑只能量化对象不能量化谓词或函数。有些程序性质涉及对于所有函数f这就超出了一阶逻辑的范围。高阶逻辑工具存在但自动化程度远不如一阶逻辑工具。第三个边界是计算复杂性。即使性质能写出来求解也可能不可判定。比如带乘法的整数算术一阶逻辑的可满足性是不可判定的。实际工具通常限制在可判定的片段比如线性算术、位向量、数组理论。我在选择验证工具的时候会先评估要验证的性质属于哪个片段。如果是线性算术加数组z3能处理得很好如果涉及非线性算术可能就需要交互式定理证明器自动化程度低很多。这个评估步骤能省下大量试错时间。9. 从一阶逻辑到实际项目的落地建议如果你打算在实际项目中引入基于一阶逻辑的验证我有几条建议。第一条是从小处着手。不要一上来就验证整个系统先选一个核心模块最好是纯函数、没有副作用的。这样翻译和验证都简单能快速看到效果。第二条是把不变式当成文档。写循环不变式的过程其实是在梳理代码的逻辑。即使不做形式化验证把不变式写在注释里对代码可读性也有帮助。我现在的习惯是写复杂循环的时候先写不变式再写循环体思路会清晰很多。第三条是接受不完整性。自动验证不可能证明所有性质总有一些需要人工介入。把自动验证当成一个筛子筛掉大部分明显错误剩下的靠人工审查。这个定位比追求全自动更现实。第四条是关注反例的质量。一个好的验证工具不仅能判断性质是否成立还能在性质不成立时给出可理解的反例。反例的质量直接影响调试效率。选择工具的时候可以先用几个已知有bug的程序测试看反例是否容易理解。最后一条是持续集成。把验证步骤加入CI流程每次代码变更都跑一遍验证。这样能及时发现回归问题。验证可能比较慢可以只对核心模块做验证或者用增量验证技术减少重复工作。一阶逻辑是程序验证的基石掌握它之后你会发现很多验证工具的设计思路变得清晰了。工具会更新换代但底层的逻辑原理相对稳定。花时间理解一阶逻辑是一笔长期投资。