Dafny新手求助：断言违反错误排查及整数平方非负断言编写

嘿，作为Dafny新手踩这个坑很正常，我来帮你拆解问题所在：

首先先把你的代码贴出来方便分析：

method Fred () returns (result : int) { 
  var number : int; 
  result := number * number; 
  assert result > 0; 
}

核心错误原因有两个： #

• 断言条件和你的意图完全不符
  你想表达的是「任意整数的平方非负」，但你写的断言是result > 0——这明显站不住脚！因为0的平方是0，0并不满足“大于0”的条件。当number取0的时候，result就是0，直接违反了这个断言，Dafny的验证引擎立刻就能找到这个反例，所以触发了断言错误。你应该把断言改成result >= 0，这才准确对应“非负”的要求。

• 未初始化的变量让Dafny考虑到了所有可能的整数取值
  在Dafny中，局部变量如果没有显式赋值，它的取值会覆盖整个整数域的所有可能值（包括0、正数、负数）。Dafny的验证逻辑会检查是否存在某个取值让断言不成立，而0就是这样的一个反例，这也是它触发错误的直接原因。

修复建议 #

如果你只是想验证“整数平方非负”这个逻辑，更规范的方式是使用Dafny的lemma（引理），因为引理专门用来证明通用的数学性质：

lemma SquareNonNegative(x: int)
  ensures x * x >= 0
{
  // Dafny的内置逻辑可以自动证明这个引理，不需要额外写证明代码
}

如果一定要用method来实现，修正断言即可：

method Fred() returns (result: int) {
  var number: int;
  result := number * number;
  assert result >= 0; // 修正断言条件
}

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