Почему неправильный пример счетчика верификатора Дафни? - PullRequest
Новая
       17

Почему неправильный пример счетчика верификатора Дафни?

0 голосов
/ 19 апреля 2020

Я пытаюсь выполнить упражнение, как описано позже в следующем видео: https://www.youtube.com/watch?v=-_tx3lk7yn4

Метод должен реализовывать BinarySearch, а когда ключ не найден, он должен возвращать индекс где ключ будет в конечном итоге, если вставить в искомый массив. Я считаю, что правильная дополнительная спецификация для упражнения выглядит следующим образом: 

ensures 0 <= r <= a.Length
ensures forall i :: 0 <= i < r ==> a[i] < key
ensures forall i :: r < i < a.Length ==> a[i] >= key

Моя реализация: 

method BinarySearch(a: array<int>, key: int) returns (r: int) 
    requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j] // a is a sorted array
    // old specification
    //ensures 0 <= r ==> r < a.Length && a[r] == key // when found a[r] is key
    //ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key // when no key found return negative value

    // restrictions for simpler debugging
    requires a.Length == 2
    requires forall i :: 0 <= i < a.Length ==> 0 <= a[i] < 5

    // new specification
    ensures 0 <= r <= a.Length // "it will always return some indication between 0 and the length of the array inclusive"
    ensures forall i :: 0 <= i < r ==> a[i] < key // "all values to the left of the value R that you're returning are strictly smaller than the key"
    ensures forall i :: r < i < a.Length ==> a[i] >= key // "from all values to the right of R is either the key or larger"
{
    // simple/common cases first
    // if array is empty
    if a.Length == 0
    {
        return 0;
    }
    // if key larger than largest
    else if key > a[a.Length - 1]
    {
        return a.Length;
    }
    // if key equal or smaller than smallest
    else if key <= a[0]
    {
        return 0;
    }
    // key is in array range
    var lo, hi := 0, a.Length;
    while lo < hi
        decreases hi - lo
        invariant 0 <= lo <= hi <= a.Length
        invariant forall i :: 0 <= i < lo ==> a[i] != key
        invariant forall i :: hi <= i < a.Length ==> a[i] != key
    {
        var mid := (lo + hi) / 2;
        if key < a[mid]
        {
            hi := mid;
        }
        else if a[mid] < key
        {
            lo := mid + 1;
        }
        else
        {
            // key found, decrease while preceding value is equal
            while mid != 0 && a[mid-1] == a[mid]
                decreases mid
                invariant 0 <= mid < a.Length
                invariant lo < hi
                invariant forall i :: 0 <= i < lo ==> a[i] != key
                invariant forall i :: hi <= i < a.Length ==> a[i] != key
            {
                mid := mid - 1;
            }
            return mid;
        }
    }
    return lo;
}

Моя проблема в том, что верификатор говорит, что спецификации не выполняются, а затем дает мне встречный пример, который не может произойти в первую очередь:

bad counter example

Я подозреваю, что в то время как у-l oop (s) отсутствуют спецификации, но я Понятия не имею, какие пробелы даже заполнить.

Использование самых последних визуальных кодов и плагинов Dafny.

...