Утверждение о возвращаемом значении метода, включающего последовательности - PullRequest
Новая
       68

Утверждение о возвращаемом значении метода, включающего последовательности

3 голосов
/ 23 мая 2019

Я начинающий с Дафни, и мне интересно, почему утверждение перед печатью в методе Main нарушается.Я пытаюсь найти самый правый индекс, в который необходимо вставить элемент, чтобы сохранить порядок в последовательности, которая в данном конкретном случае равна 4.

https://rise4fun.com/Dafny/4lR2

method BinarySearchInsertionHint(a: seq<int>, key: int) returns (r: int) 
    requires forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j]
    ensures 0 <= r <= |a|
    ensures forall i :: 0 <= i < r ==> a[i] <= key
    ensures r < |a| ==> forall i :: r <= i < |a| ==> key < a[i]
{
    var lo, hi := 0, |a|;
    while lo < hi
        decreases hi - lo
        invariant 0 <= lo <= hi <= |a|
        invariant forall i :: 0 <= i < lo ==> a[i] <= key
        invariant forall i :: hi <= i < |a| ==> key < a[i]
    {
        var mid := (lo + hi) / 2;
        assert(lo <= mid < hi);
        if a[mid] <= key {
            lo := mid + 1;
        } else if key < a[mid] {
            hi := mid;
        }
    }
    assert(lo == hi);
    r := lo;
}

method Main() {
    var a := [0, 1, 1, 1, 2];
    var hint := BinarySearchInsertionHint(a, 1);
    assert hint == 4; // assertion violation
    print hint;
}

1 Ответ

3 голосов
/ 23 мая 2019

Это действительно может сбить с толку!Здесь происходит несколько вещей:

Во-первых, помните, что Дафни рассуждает о каждом методе отдельно, используя только спецификации других методов.Так что в Main единственное, что Дафни узнает о BinarySearchInsertionHint, это его постусловия.Теперь получается, что hint == 4 на самом деле действительно следует из постусловий, но убедить Дафни в этом немного нетривиально.

Это подводит нас ко второму действию, происходящему здесь, которое является триггером-квантификатором.В постсекундах BinarySearchInsertionHint используются универсальные квантификаторы (forall), которые Дафни рассуждает об использовании синтаксической эвристики для создания экземпляров.Оба квантификатора в этом примере запускаются на a[i], что означает, что они не будут использоваться со значением v , если a[v] не находится в области действия для верификатора.

Вы можете получить утверждение, упомянув a[3] и a[4], чего достаточно для Дафни из постусловий выяснить, что hint должно быть 4.Например: 

method Main() {
    var a := [0, 1, 1, 1, 2];
    var hint := BinarySearchInsertionHint(a, 1);
    assert a[3] == 1;  // these assertions just "mention" a[3] and a[4]
    assert a[4] == 2;
    assert hint == 4;  // assertion now passes
    print hint;
}

Подробнее о модульных проверках Дафни, триггерах и неполных количествах можно узнать в Dafny FAQ .

...