Дафни программа не может доказать эту реализацию бинарного поиска? - PullRequest
Новая
       9

Дафни программа не может доказать эту реализацию бинарного поиска?

0 голосов
/ 17 декабря 2018

Мы пытаемся написать алгоритм двоичного поиска, используя Дафни, и кажется, что Дафни не доказывает правильность программы.

Может кто-нибудь помочь?Вот ошибки, которые мы получаем:

При INV: этот инвариант цикла может не поддерживаться циклом. Дафни VSCode

В Guard1: уменьшение выражения может не уменьшаться Дафни 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;
    }
}

1 Ответ

0 голосов
/ 18 декабря 2018

Верификатор 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.

Последнее замечание.Возможно, вам пригодится следующий эпизод «Проверочного угла»: https://www.youtube.com/watch?v=-_tx3lk7yn4

Rustan

...