Ошибка BP5005: этот инвариант l oop может не поддерживаться циклом

Question

Я новичок в Дафни. Я не понимаю, почему я получаю это сообщение с x == Sum(i);, я начинаю сходить с ума. А также почему он компилируется, когда if n==0 then 0 else n + Sum(n-1) превращается в if n==0 then 0 else n-1 + Sum(n-1)

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

method ComputeSum(n: nat) returns (x: nat) 
  ensures x == Sum(n);
{
  x := 0;
  var y := 0;
  var i : nat := 0;
    while i < n
      invariant 0 <= i <= n && x == Sum(i);
    {
      x,y := y,x + y ;
      i := i + 1;

    }
 }

Answer 1

По поводу вашего второго вопроса: если вы измените if n==0 then 0 else n + Sum(n-1) на if n==0 then 0 else n-1 + Sum(n-1), значение Sum (n) будет 0 для каждого n. И это соответствует ComputeSum, который возвращает 0 для всех входов n.

Answer 2

Вы устанавливаете x и y в 0, но никогда не увеличиваете их, поэтому добавление остается равным 0. Дафни, правильно, доказывает, что ваша программа не удовлетворяет спецификации. Я бы посоветовал вам пройтись по вашей программе за небольшим n, чтобы исправить ошибку.