小编Dee*_*Dee的帖子

我正在将我在 Dafny 中做的一项练习翻译成 SPARK，其中验证尾递归函数与递归函数。Dafny 源代码（经过审查，因为它可能仍用于类）：

function Sum(n:nat):nat 
    decreases n
{ 
    if n==0 then n else n+Sum(n-1)
}

method ComputeSum(n:nat) returns (s:nat) 
    ensures s == Sum(n) 
{
    s := 0;
    // ...censored...
}

到目前为止我在 SPARK 中得到了什么：

function Sum (n : in Natural) return Natural
is
begin
   if n = 0 then
      return n;
   else
      return n + Sum(n - 1);
   end if;
end Sum;

function ComputeSum(n : in Natural) return Natural
  with
    Post => ComputeSum'Result = Sum(n)
is
   s : Natural …