Не уверен, почему эта проверка Дафни не удалась

function method abs(m: int): nat
{ if m>0 then m else -m }

method CalcTerm(m: int, n: nat) returns (res: int)
  ensures res == 5*m-3*n;
{
  var m1: nat := abs(m);
  var n1: nat := n;
  res := 0;

  while (m1!=0)
    invariant m1>=0
    invariant 0<=res
    invariant res <=5*abs(m)
    decreases m1
  {
    res := res+5;
    m1 := m1-1;
  }
  if (m<0) { res := -res; }

  while (n1!=0)
    invariant n1>=0 
    decreases n1
  {
    res := res-3;
    n1 := n1-1;
  }
}

Я попытался увеличить инвариантность в петлях. К первому циклу я добавил условие res‹=5*abs(m), но Дафни жалуется, что «этот инвариант цикла может не поддерживаться циклом». Я не понимаю, как это не так.

Что я могу делать неправильно?


dafny
person user714023    schedule 26.03.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Если вы укрепите свой инвариант цикла, точно указав, чему равно res после каждой итерации, Дафни сможет это проверить.

Итак, в первом цикле вместо invariant res <= 5*abs(m) используйте invariant res == 5*abs(m) - 5*m1. Когда цикл завершается, m1 равно нулю, поэтому res будет 5*abs(m).

Точно так же для второго цикла while определите invariant res == 5*m - 3*n + 3*n1. Теперь, когда этот цикл завершается, n1 равно нулю, поэтому res будет 5*m - 3*n, и Дафни сможет доказать, что постусловие метода выполняется.

P.S. Обычно я использую > 0 вместо != 0 в качестве условия цикла.

После внесения этих изменений у вас будет:

function method abs(m: int): nat
{
    if m > 0 then m else -m
}

method CalcTerm(m: int, n: nat) returns (res: int)
    ensures res == 5*m - 3*n;
{
    var m1: nat := abs(m);
    var n1: nat := n;
    res := 0;

    while (m1 > 0)
        invariant m1 >= 0;
        invariant 0 <= res;
        invariant res == 5*abs(m) - 5*m1;
        decreases m1;
    {
        res := res + 5;
        m1 := m1 - 1;
    }
    if (m < 0)
    {
        res := -res;
    }

    while (n1 > 0)
        invariant n1 >= 0;
        invariant res == 5*m - 3*n + 3*n1;
        decreases n1;
    {
        res := res - 3;
        n1 := n1 - 1;
    }
}

который проверяет в Дафни.

person Watermelon    schedule 28.03.2020