Покажи сумбурную ровность в Дафни

Вот код, который я пытаюсь доказать:

function rec_even(a: nat) : bool
  requires a >= 0;
{
   if a == 0 then true else
   if a == 1 then false else
                  rec_even(a - 2)
}


method Even(key: int) returns (res: bool)
  requires key >= 0;
  ensures res == rec_even(key)
{   
  var i : int := key;
  while (i > 1)
    invariant  0 <= i <= key;
    decreases i;
  {
    i:= i - 2;
  }
  res := i == 0;
}

Но я получаю сообщение об ошибке постусловия:

stdin.dfy (13,0): Ошибка BP5003: Постусловие может не выполняться на этом пути возврата. stdin.dfy (12,14): Связанное местоположение: это постусловие, которое может не выполняться.

Если есть способ доказать зацикленную версию четности (цикл while или рекурсивный), я был бы признателен!

РЕДАКТИРОВАТЬ: это может быть неочевидно из кода, но я ищу индуктивное доказательство n, которое dafny должно иметь возможность выяснить, по крайней мере, для случая метода.

Я видел несколько подобных доказательств того, что рекурсивная функция используется в инварианте цикла функции метода, просто не знаю, почему она не работает в этом конкретном случае.

Вы можете попробовать код на rise4fun здесь: https://rise4fun.com/Dafny/wos9


formal-verification dafny
person rausted    schedule 17.03.2018    source источник
comment
Надеюсь, добавлена ​​ссылка rise4fun, которая упростит получение помощи.   -  person rausted    schedule 20.03.2018

Ответы (1)


arrow_upward
3
arrow_downward

Я вижу проблему с доказательством постусловия вашей реализации, если вы начнете с нуля, вы можете установить инвариант цикла для 0 и перейти оттуда.

function rec_even(a: nat) : bool
    decreases a
{
    if a == 0 then true else
    if a == 1 then false else
    rec_even(a - 2)
}

lemma {:induction a} Lemma(a:int)
    requires 1 <= a
    ensures rec_even(a-1) ==> !rec_even(a)
    {

    }

method Even(n: int) returns (res: bool)
requires n >= 0;
ensures res == rec_even(n)
{   
    var i : int := 0;
    while (i < n)
        invariant  0 <= i <= n+1;
        invariant rec_even(i)
        decreases n-i;
    {
        i:= i + 2;
    }
    assert rec_even(i);
    Lemma(i+1);
    assert i == n ==> rec_even(n);
    assert i == n+1 ==> !rec_even(i+1);
    res := i == n;
}

Последний шаг требует леммы, чтобы установить отрицательный случай из двух возможных случаев в конце для i, (i == n) или (i == n + 1).

Надеюсь, поможет.

person Joao Costa Seco    schedule 20.03.2018