公理语义

公理语义把程序视为状态性质之间的变换器，而不是一串机器步骤。证明从目标后置条件反推每条语句执行前必须满足什么，或从已知前置条件向前维护不变量。推理规则刻画程序构造如何组合证明，因此一份验证可以按语法模块化。它刻意忽略许多实现细节，只保留与所声明性质有关的逻辑关系；这使证明简洁，也意味着性能和中间事件需要其他语义工具。

要证明 $\{x=0\}x:=x+1\{x=1\}$，赋值公理要求前置条件为 $(x+1=1)$，即 $x=0$，恰好满足。对顺序程序 x:=x+1; y:=2*x，可选择中间断言连接两次赋值，再用顺序规则合成。

边界是循环：仅靠展开语句无法完成有限证明，需要用户或工具提供循环不变量。断言语言若无法表达某个必要不变量，即使程序性质语义上成立，系统也可能无法推导。部分正确性还允许程序永不终止，因此不能把三元组自动读成“程序一定产生 $Q$ 状态”。

公理语义以Hoare 三元组公理库Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。为核心，最弱前置条件公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。把规则变成系统化验证条件生成。分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。进一步把状态断言扩展为可分堆资源，支持指针程序的局部推理。

这套方法把程序正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。目标分解成可组合的证明义务。基于 SMT 的软件验证公理库基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。把程序注解与路径条件转化为理论公式，再让求解器寻找反模型；这是一条自动化实现链，不会把公理语义的规则有效性变成“求解器说真”。规则可靠性仍须相对于操作语义公理库操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。证明，生成器还须覆盖程序的每条控制流路径。