Постусловие для метода поиска минимального значения массива
У меня есть функция, чтобы найти минимальное значение массива
method arrayMin(a: array<int>) returns (m: int)
requires a.Length > 0;
ensures forall k :: 0 <= k < a.Length ==> a[k] >= m;
{
var i: nat := 1 ;
m := a[0] ;
while (i < a.Length)
invariant 1 <= i <= a.Length && forall k :: 0 <= k < i ==> a[k] >= m;
decreases a.Length - i;
{
if (a[i] < m) { m := a[i] ; }
i := i + 1 ;
}
}
Когда я пытаюсь вызвать
var a := new int[5];
a[0], a[1], a[2], a[3], a[4] := 9, 4, 6, 3, 8;
var min := arrayMin(a);
assert min == 3;
Дафни сможет проверить это утверждение. Почтовые условия недостаточны?
Ответы 1
Вы правы, что постусловие недостаточно. На английском языке постусловие говорит следующее:
Ни один элемент в массиве
aне ниже возвращаемого значенияm.
Но это не значит, что m должно быть значением из исходного массива! Например, мы можем безопасно изменить эту строку:
if (a[i] < m) { m := a[i] ; }
Быть таким:
if (a[i] < m) { m := a[i] - 1; }
И эта программа все равно будет соответствовать постусловию.
Поэтому, чтобы ваше утверждение прошло, вам понадобится более сильное постусловие. В частности, необходимо убедиться, что m является одним из элементов, содержащихся в a.
Это правильно. Проблема сейчас в том, что Дафни не может собрать информацию воедино, чтобы проверить утверждение. Мы должны помочь этому. Чтобы проверить это, я добавил assert forall k :: 0 <= k < a.Length ==> a[k] >= min; непосредственно перед утверждением.
После добавления пост-условия гарантируется, что существует k :: 0 <= k < a.Length && a[k] == m; утверждение все еще не может быть проверено