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

Я новичок в Dafny, и мне интересно, почему нарушается утверждение непосредственно перед печатью в методе 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;
}

seq formal-verification dafny
person lilezek    schedule 23.05.2019    source источник

Ответы (1)


arrow_upward
3
arrow_downward

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

Во-первых, помните, что Дафни рассуждает о каждом методе отдельно, используя только спецификации других методов. Итак, в 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. .

person James Wilcox    schedule 23.05.2019