为何Dafny验证存在逻辑矛盾的max函数代码？如何设计教学练习？

一、为什么max(2,4) == 4的断言能被Dafny验证通过？ #

核心原因是逻辑爆炸原理——当逻辑前提存在矛盾时，任何命题都可被证明：

1. 你的max函数被标记为{:axiom}，这意味着Dafny会将函数的所有后置条件当作无需证明的逻辑公理。
2. 当前的后置条件存在明显矛盾：
   • 第一个条件要求max(a,b) >= a && max(a,b) >= b，代入a=2, b=4时，必然要求max(2,4) >=4；
   • 第二个条件却强制max(a,b) == a，也就是max(2,4) ==2。
3. 2不可能大于等于4，这两个公理无法同时成立，此时整个逻辑体系陷入矛盾。在经典逻辑中，矛盾的前提可以推导出任意结论——不光是max(2,4)==4，哪怕你写max(2,4)==100，Dafny也会验证通过。

简单来说：你的公理自相矛盾，验证器失去了判断依据，只能默认所有断言成立。

二、高中进阶CS课程的练习优化方案 #

结合高中生的认知规律，设计分层递进的练习，让学生从理解到实践，逐步掌握形式化验证的核心逻辑：

1. 前置铺垫：建立对后置条件的直观认知 #

• 先展示无后置条件的max函数，让学生尝试编写断言，观察Dafny无法验证任何关于max结果的命题——以此让学生明白：后置条件是给验证器的“规则说明书”，没有它，验证器不知道函数该满足什么约束。
• 引入矛盾后置条件的小实验：让学生故意写出自相矛盾的规则，观察所有断言都能通过，引导他们发现“自相矛盾的规则等于没有规则”。

2. 核心练习：补全规则+验证修正 #

• 给出你提供的有缺陷的max函数代码，先让学生完成两个任务：
  • 分析为什么max(2,4)==4能通过验证；
  • 找出当前后置条件的缺失部分。
• 让学生补全后置条件（添加|| max(a,b) == b），然后要求他们修改测试方法：
  • 保留正确的断言（如max(3,2)==3、max(2,4)==4）；
  • 添加错误断言（如max(2,4)==2），观察Dafny会报错，以此验证补全后的后置条件能精准约束函数行为。

3. 拓展变式：从单一函数到复杂场景 #

• 变式1：让学生为min函数设计完整的后置条件，并用相同的测试逻辑验证；
• 变式2：进阶到数组的max函数（如ghost function arrayMax(arr: array<int>) : int），要求学生写出包含“结果是数组中的元素”、“结果大于等于数组所有元素”的后置条件；
• 变式3：引入前置条件（如要求数组非空），让学生理解前置条件是函数的“输入准入规则”，后置条件是“输出承诺”。

4. 互动环节：分组找茬与验证 #

• 将学生分成小组，每组给对方编写带有缺陷后置条件的函数，另一组需要找出问题并修正，同时用断言验证修正后的正确性——通过互动强化对形式化验证逻辑的理解。

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