dafny 断言违反错误，不知道是什么原因

Question

我对 Dafny 很陌生。它在这里抱怨有一个断言错误：

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

}

我正在尝试编写一个断言来表达以下语句：任何整数的平方都是非负的

Answer 1

如果将断言更改为result >= 0，则断言通过。这是你的意思吗？如果number 为0，那么result 也将为0。