Модель Z3 для правильного метода Дафни

Question

Для правильного метода может ли Z3 найти модель для условия проверки метода?

Я не думал, но вот пример, когда метод является правильным

пока проверка находит модель.

Это было с Dafny 1.9.7.

Answer 1

Что говорит Malte правильно (и я нашел, что это хорошо объяснил, как хорошо) ,

Dafny звучит в том смысле, что он будет проверять только правильные программы. Другими словами, если программа неверна, верификатор Dafny никогда не скажет, что это правильно. Однако основные проблемы решения в целом неразрешимы. Следовательно, неизбежно будут случаи, когда программа соответствует ее спецификациям, и верификатор все еще выдаёт сообщение об ошибке. Действительно, в таких случаях верификатор может даже показать контрпримерный пример . Это может быть ложный контрпример (как в примере выше) - это просто означает, что, насколько может сказать верификатор, это контрпример. Если верификатор просто потратил немного больше времени или если он был достаточно умен, чтобы развернуть больше определений функций, применить гипотезы индукции или сделать множество других полезных дел, возможно, будет возможно определить, что контрпример является фиктивным , Таким образом, любое сообщение об ошибке, которое вы получаете (включая любой контрпример, который может сопровождать такое сообщение об ошибке), должно интерпретироваться как возможное ошибка (и возможно counterexample).

Подобные ситуации часто возникают, если вы пытаетесь проверить правильность цикла, и вы не обеспечиваете достаточно сильного инварианта цикла. Затем верификатор Dafny может показывать некоторые значения переменных при входе в цикл, которые никогда не могут произойти в действительности. Контрпример затем пытается дать вам представление о том, как укрепить ваш инвариант цикла соответствующим образом.

Наконец, позвольте мне добавить две заметки к тому, что сказал Малте.

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

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

lemma EvenPowerLemma(a: int, b: nat) 
    requires Even(b) 
    ensures Pow(a, b) == Pow(a*a, b/2) 
{ 
    if b != 0 { 
    var dummy := Pow(a, b - 2); 
    } 
} 

Тем не менее, мне нравятся две другие ручные доказательства лучше, потому что они делают лучше объяснить пользователю, что доказательство.

Rustan

Answer 2

Dafny не может доказать лемму из-за сочетания двух возможных источников неполноты: рекурсивных определений (здесь Pow) и индукции. Доказательство эффективно терпит неудачу из-за слишком малой информации, т. Е. Потому что проблема недостоверна, что, в свою очередь, объясняет, почему встречный пример можно найти.

Индукция

индукция автоматизации сложно, поскольку это требует вычисления индукции, что не всегда возможно. Тем не менее, Dafny имеет некоторые эвристики для применения индукции (что может или не может работать), и которые могут быть включены в, как показано в следующем коде:

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat) 
    requires Even(b); 
    ensures Pow(a, b) == Pow(a*a, b/2); 
{ 
    if (b != 0) { 
    EvenPowerLemma_manual(a, b - 2); 
    } 
} 

С эвристики выключенными, вам нужно вручную «называть» лемму, т. е. использовать индукционное предположение (здесь, только в случае, когда b >= 2), чтобы получить доказательство.

В вашем случае были активированы эвристики, но они не были «достаточно хороши», чтобы получить доказательство. Я объясню, почему дальше.

Рекурсивных определений

Рассуждая статический о рекурсивных определениях, разворачивая их склонен к бесконечному спуску, потому что это вообще неразрешимому, когда остановиться. Следовательно, Dafny по умолчанию разворачивает определения функций только один раз. В вашем примере развернуть определение Pow только один раз недостаточно, чтобы заставить эвристику индукции работать, потому что гипотеза индукции должна применяться к Pow(a, b-2), которая не «появляется» в доказательстве (поскольку разворачивание однажды приведет вас только к Pow(a, b - 1)) , Явное упоминание Pow(a, b-2) в доказательстве, даже в противном случае бессмысленной формулы, вызывает индукционные эвристики, однако:

function Dummy(a: int): bool 
{ true } 

lemma EvenPowerLemma(a: int, b: nat) 
    requires Even(b); 
    ensures Pow(a, b) == Pow(a*a, b/2); 
{ 
    if (b != 0) { 
    assert Dummy(Pow(a, b - 2)); 
    } 
} 

Dummy функции есть, чтобы убедиться, что утверждение не дает никакой информации, кроме синтаксический включая Pow(a, b-2). Менее странно выглядящим утверждением будет assert Pow(a, b) == a * a * Pow(a, b - 2).

Расчетные Proof

FYI: Вы можете также сделать доказательство шаги явной и иметь Dafny проверить их:

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat) 
    requires Even(b); 
    ensures Pow(a, b) == Pow(a*a, b/2); 
{ 
    if (b != 0) { 
    calc { 
     Pow(a, b); 
     == a * Pow(a, b - 1); 
     == a * a * Pow(a, b - 2); 
     == {EvenPowerLemma_manual(a, b - 2);} 
     a * a * Pow(a*a, (b-2)/2); 
     == Pow(a*a, (b-2)/2 + 1); 
     == Pow(a*a, b/2); 
    } 
    } 
}