Dafny中函数与方法在assert语句中的行为差异原因探究

Dafny对方法（method）和函数（function）的验证逻辑存在本质区别，这直接导致了你遇到的现象：

• 函数的验证逻辑：函数是纯无副作用的计算，验证器可以直接展开函数体进行符号计算。调用absfunction(3)时，验证器会直接算出结果为3，因此断言v2==3能直接通过验证。

• 方法的验证逻辑：方法代表可执行的过程，验证器仅依赖你声明的契约（ensures后置条件）进行推理，不会分析方法内部的实现细节。你的absmethod只声明了返回值y>=0，没有明确返回值与输入x的具体关系，所以验证器仅知道v1是非负整数，但无法确定它等于3，因此断言v1==3会提示不成立。

解决方法 #

给absmethod补充更精确的后置条件，让验证器能推导出返回值的具体属性：

method absmethod(x:int) returns (y:int)
  ensures 0<=y
  ensures y == if x < 0 then -x else x  // 明确返回值与输入的关系
{
  if x<0 {y:=-x;} else {y:=x;}
}

或者借助已有的函数来简化契约：

method absmethod(x:int) returns (y:int)
  ensures 0<=y
  ensures y == absfunction(x)  // 复用函数的定义
{
  if x<0 {y:=-x;} else {y:=x;}
}

补充契约后，验证器就能通过后置条件推导出v1==3，断言即可通过验证。

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