Дафни поддерживает «доказательство по построению»? - PullRequest
Новая
       6

Дафни поддерживает «доказательство по построению»?

0 голосов
/ 01 июня 2018

Предположим, у меня есть метод, который что-то вычисляет: 

method Difference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  ...
}

Не берите в голову реализацию на данный момент.Если я могу реализовать этот метод в Dafny, это означает, что для всех возможных аргументов a и b должно быть некоторое возвращаемое значение c который удовлетворяет постусловию.

Другими словами, тело метода является конструктивным доказательством , что: 

forall a: nat, b: nat :: exists c: nat ::
  a + c == b || b + c == a

Но Дафни не убежден: 

method Difference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  c := if a > b then a - b else b - a;
}

method Main() {
  assert forall a: nat, b: nat :: exists c: nat ::  // error: assertion violation :(
    a + c == b || b + c == a;
}

Есть ли способ использовать подобные рассуждения в Дафни?

Ответы [ 2 ]

0 голосов
/ 04 июня 2018

Ответ Валери - хороший трюк для случаев, когда существование доказано леммой.Вы также можете расширить трюк до «подсказки внутри forall», используя оператор forall Дафни , например, 

forall a: nat, b: nat
    ensures exists c: nat :: difference_property(a, b, c)
{
    var c := difference(a, b);
    assert difference_property(a, b, c);
}

, который подтверждает выражение forall 

forall a: nat, b: nat :: 
    exists c: nat :: 
        difference_property(a, b, c)

В связи с другим вопросом Джейсона об использовании правильных методов в доказательствах Дафни не поддерживает это.Действительно, я думаю, что имеет смысл, что это не поддерживается, так как, например, методы могут оказывать влияние на кучу.Таким образом, построение какого-либо свидетеля может в принципе зависеть от распределения состояния или даже изменения существующего состояния.Внедрение этого эффекта в логику подозрительно и изменит характер Дафни.

0 голосов
/ 02 июня 2018

Это делает трюк: оберните свойство в предикат и докажите exists в лемме, так что вы можете намекнуть верификатору с помощью assert.

Может быть, есть какой-то способподсказка внутри forall. 

predicate difference_property(a: nat, b: nat, c: nat)
{
    a + c == b || b + c == a
}

function difference(a: nat, b: nat): nat
{
    if a > b then a - b else b - a
}

lemma main(a: nat, b: nat)
    ensures exists c: nat :: difference_property(a, b, c)
{
    var c := difference(a, b);
    assert difference_property(a, b, c);
}
...