为何Dafny使用不成立的assume时能验证通过assert语句？

核心矛盾与空洞真 #

你使用的程序验证工具（如Dafny）会将带{:axiom}属性的assume语句视为无需验证的全局公理。在初始代码中：

• 先给z赋值为-1，紧接着用assume {:axiom} z>0;强制验证器认定z>0为真，这就制造了逻辑矛盾——没有任何实际值能同时满足z=-1和z>0。
• 根据逻辑中的“爆炸原理”，从矛盾的前提可以推导出任意结论，所以assert y>0会被判定为空洞成立（即没有可行路径能触发断言失败），方法自然能通过验证。

正常验证的情况 #

当你把z的赋值改为1时：

• 此时z=1和assume {:axiom} z>0;的约束一致，上下文没有矛盾，验证器会基于真实的变量范围进行推理。
• 由于x是任意整数（例如x=-3时，y=1+(-3)+1=-1），存在大量输入会导致y≤0，所以assert y>0无法通过验证，验证器会提示断言可能不成立。

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