Что не так с моим dafny методом. постусловие простого метода может не выполняться
Я новичок в Dafny и пытаюсь написать код для компьютера 5*m-3*n без использования *.
Кто-нибудь может сказать мне, что не так с моим кодом? Я думаю, что это инвариант и уменьшение.
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
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;
}
}
Но он продолжает говорить, что:
A postcondition might not hold on this return path. 29 2
Ответы 1
Вы правы, что проблема связана с инвариантами цикла. Я рекомендую прочитать два раздела Гид об утверждениях и инвариантах цикла.
Дафни «обобщает» эффект цикла, используя его инварианты Только. Таким образом, после второго цикла в вашем методе Дафни будет знать только, что n1 >= 0 и что цикл завершился, так что на самом деле n1 == 0. Этой информации недостаточно для доказательства вашего постусловия: вам нужен более сильный инвариант. Вот тот, который может помочь вам добиться прогресса
invariant res == 5 * m - 3 * (n - n1)
Этот инвариант вычисляет значение res с точки зрения того, сколько итераций цикла выполнено до сих пор (n - n1). Если вы добавите этот инвариант во второй цикл, вы получите новую ошибку (прогресс!), в которой говорится, что запись может не удерживаться. Это означает, что Дафни может доказать ваше постусловие, но не может установить, что новый инвариант верен после выполнения первого цикла. Это опять же потому, что инвариант в первом цикле слишком слаб.
Возможно, это даст вам достаточно информации, чтобы попытаться самостоятельно придумать другой инвариант для первого цикла. Не стесняйтесь задавать здесь дополнительные вопросы, если вы застряли.
Учитывая числовую природу этой проблемы, вам может помочь следующий эпизод Verification Corner, где пример представляет собой аналогичную проблему: youtube.com/watch?v=spcfzbisBv4
Спасибо. Я узнаю определение инварианта и уже решил его с вашей помощью.