Мы пытаемся написать алгоритм двоичного поиска с использованием Dafny, и кажется, что Dafny не доказывает правильность программы.
может кто-нибудь помочь? Мы получаем следующие ошибки:
On INV: этот инвариант цикла может не поддерживаться циклом. Dafny VSCode
На Guard1: выражение уменьшения может не уменьшаться Dafny VSCode
predicate Sorted(q: seq<int>)
{
forall i,j :: 0 <= i <= j < |q| ==> q[i] <= q[j]
}
method BinarySearch(q: seq<int>, key: int) returns (j: nat)
requires Sorted(q) && key in q
ensures j < |q| && q[j] == key
{
var i: nat, k: nat;
i,j,k := Init(q,key);
while Guard1(q,key,j)
invariant Inv(q,key,i,j,k)
decreases V(i,k)
{
if Guard2(q,key,j)
{
i := UpdateI(q,key,i,j,k);
}
else
{
k := UpdateK(q,key,i,j,k);
}
j := (i+k)/2;
}
}
predicate Inv(q: seq<int>, key: int, i: nat, j: nat, k: nat)
{
i <= j <= k < |q| &&
key in q[i..k+1]
}
predicate method Guard1(q: seq<int>, key: int, j: nat)
requires Sorted(q) && key in q
{
0 <= j < |q| && q[j] != key
}
method Init(q: seq<int>, key: int) returns (i: nat, j: nat, k: nat)
requires Sorted(q) && key in q
ensures 0 <= i <= j <= k < |q| && key in q[i..k+1]
{
i, k := 0, |q|-1;
j := (k+i) / 2;
}
function V(i: nat, k: nat): int
{
if (k > i) then k-i
else 0
}
predicate method Guard2(q: seq<int>, key: int, j: nat)
{
0 <= j < |q| && q[j] < key
}
method UpdateI(q: seq<int>, key: int, i0: nat, j: nat, k: nat) returns (i: nat)
requires Guard2(q,key,j) && Inv(q,key,i0,j,k)
ensures i0 <= i
{
if (j < |q|-1 ){
i:= j + 1;
}
else {
i:= j;
}
}
method UpdateK(q: seq<int>, key: int, i: nat, j: nat, k0: nat) returns (k: nat)
requires (!Guard2(q,key,j)) && Inv(q,key,i,j,k0)
ensures k <= k0
{
if (j > 0){
k:= j - 1;
}
else {
k:= j;
}
}
Верификатор Dafny рассуждает о вызовах методов UpdateI
и UpdateK
только с точки зрения их спецификаций. Постусловие, которое вы дали этим двум методам, недостаточно сильное, чтобы доказать прекращение. В частности, UpdateI(..., i, ...)
может возвращать i
, а UpdateK(..., k, ...)
может возвращать k
, и в этом случае ваш цикл не продвинется.
У меня есть еще два предложения.
Один, возможно, дело вкуса, но я считаю, что он упрощает выражения. Используйте k
как самый низкий из неиспользуемых индексов, а не как самый высокий из используемых индексов. Итак, инициализируйте k
как |q|
, а не как |q|-1
. Таким образом, каждая итерация цикла просматривает элементы k-i
(не k-i+1
), начиная с индекса i
. То есть смотрит на q[i..k]
(а не на q[i..k+1]
).
Во-вторых, вашу программу действительно трудно читать, потому что у вас без нужды есть отдельные функции и методы для множества вещей. Кроме того, у этих вещей есть бессмысленные имена, такие как Guard1
, V
и UpdateI
. Я думаю, вам лучше просто написать эти выражения и утверждения непосредственно в методе BinarySearch
.
Последнее замечание. Возможно, вам будет полезен следующий выпуск Verification Corner: https://thewikihow.com/video_-_tx3lk7yn4
Рустан
Привет, Рустен, меняю k на | q | вместо | q | -1 оставляет меня с теми же ошибками. Поскольку это часть домашнего задания, я должен использовать эту структуру ненужных функций. Буду признателен за любую помощь,