Не уверен, почему эта проверка Dafny не проходит - PullRequest
Новая
       13

Не уверен, почему эта проверка Dafny не проходит

0 голосов
/ 26 марта 2020 
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;
  }
}

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

Что я могу делать не так?

1 Ответ

0 голосов
/ 28 марта 2020

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

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

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

PS Я обычно использую > 0 вместо != 0 в качестве условия oop.

После внесения этих изменений вы получите: 

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;
    }
}

, который проверяет в Dafny.

...