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

Мы пытаемся написать алгоритм двоичного поиска с использованием 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;
    }
}
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
0
0
460
1

Ответы 1

Верификатор 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 оставляет меня с теми же ошибками. Поскольку это часть домашнего задания, я должен использовать эту структуру ненужных функций. Буду признателен за любую помощь,

Orr Levy 18.12.2018 07:26

Другие вопросы по теме