Whiley中如何编写类似Dafny的引理（Lemma）实现性质证明

Whiley 没有提供和 Dafny lemma 关键字一一对应的独立语法结构，所有引理性质的证明都通过带规范约束的无副作用属性（property）/函数实现，编译时这类证明结构会被完全擦除，不会产生运行时开销，和 Dafny 引理的实际效果一致。

核心逻辑是：把引理的前提作为requires前置条件，引理要证明的结论作为ensures后置条件，函数/属性体内的分支、递归调用就是给验证器提供的证明步骤，验证器会自动检查实现是否能推导出后置条件，即完成引理证明。

针对账户转账总金额不变场景的实现步骤 #

你已经写好了递归求和的sum属性，接下来只需要两步就能完成不变式证明：

1. 先写辅助引理，证明「单个数组元素更新时，区间求和值的变化规则」
   因为sum是递归定义的，验证器无法自动推导数组修改对sum的影响，这个引理就是给验证器补全推理规则：

   // 引理：修改数组arr的i位置为new_v后，从k位置开始的sum满足固定变化规则
   property sum_update_lemma(int[] arr, int i, int new_v, int k) -> bool:
       // 前置条件：参数合法性约束
       requires 0 <= k
       requires 0 <= i && i < |arr|
       // 引理结论
       // 1. 求和起点在修改位置之后：sum完全不变
       ensures k > i ==> sum(arr{i:=new_v}, k) == sum(arr, k)
       // 2. 求和起点在修改位置之前/刚好在修改位：sum增量为新值减旧值
       ensures k <= i ==> sum(arr{i:=new_v}, k) == sum(arr, k) + (new_v - arr[i])
   :
       // 归纳证明步骤，引导验证器完成推导
       if k >= |arr|:
           // 基例：求和越界，两边sum都是0，等式成立
           return true
       else if k == i:
           // 到达修改位置，展开sum定义可直接验证成立
           return true
       else:
           // 归纳步：递归调用k+1位置的引理结论，结合sum的递归定义即可推导
           return sum_update_lemma(arr, i, new_v, k+1)
   

2. 在转账函数中调用引理，完成总金额不变的证明
   不需要额外写特殊语法，只需要在转账函数的规范里声明总金额不变的后置条件，在实现里调用上面的引理即可：

   function transfer(int[] accounts, int from_idx, int to_idx, int amount) -> (int[] res):
       // 业务前置约束
       requires 0 <= from_idx && from_idx < |accounts|
       requires 0 <= to_idx && to_idx < |accounts|
       requires amount > 0
       requires accounts[from_idx] >= amount
       // 要证明的不变式：转账后总金额不变
       ensures sum(res, 0) == sum(accounts, 0)
   :
       // 第一步：扣减转出账户余额
       int from_new = accounts[from_idx] - amount
       _ = sum_update_lemma(accounts, from_idx, from_new, 0)
       accounts[from_idx] = from_new
       // 第二步：增加转入账户余额
       int to_new = accounts[to_idx] + amount
       _ = sum_update_lemma(accounts, to_idx, to_new, 0)
       accounts[to_idx] = to_new
       return accounts
   

编写Whiley引理的实用技巧 #

• 递归定义的属性（比如你写的sum）对应的引理，尽量用和原属性同结构的递归写法，验证器的自动归纳推理通过率会高很多
• 引理不需要有实际运行时的返回值意义，返回bool类型只是为了符合property的语法要求，调用时把返回值赋给_即可，编译器会完全擦除这些调用
• 如果验证器报证明失败，可以把引理的结论拆成更细的ensures子句，在证明体里加对应分支显式验证每一个子句，不要依赖验证器自动做复杂的跨步推理

内容的提问来源于stack exchange，提问作者JimW