(Dafny) Поиск в массиве - вариант цикла, ограниченный нулем?

Рассмотрим следующий код Dafny, который пытается найти элемент e внутри массива a:

method findE(a:array<int>, e:int, l:int, u:int) returns (result:bool)
    requires a != null
    requires 0 <= l <= u < a.Length
    ensures result <==> exists k | l <= k <= u :: a[k] == e
{   
    var i := l;

    while i <= u 
        invariant l <= i <= u+1
        invariant !(exists k | l <= k < i :: a[k] == e)
        decreases u-i
    {
        if a[i] == e {
            result :=   true;
            return;
        }   
        i := i+1;
    }
    result :=   false;
}

Проверка работает нормально, но есть кое-что, чего я не уверен: если я не ошибаюсь, вариант цикла, если он целочисленный, должен быть ограничен нулем. Однако u-i опускается ниже нуля, когда i = u+1 на последней итерации. Почему Дафни не жалуется на то, что u-i не ограничено нулем?


arrays variant verification dafny
person Dory    schedule 08.06.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы правы в том, что вариант (который Дафни называет предложением уменьшения) должен быть ограничен снизу. Но Дафни допускает любую нижнюю границу, а не только 0.

В вашем случае инвариант цикла i <= u + 1 подразумевает, что -1 <= u - i, поэтому предложение уменьшения ограничено ниже.

Для получения дополнительной информации см. раздел 21.10.0.1 Dafny Reference Руководство.

person James Wilcox    schedule 29.07.2017