Дафни: более сильное утверждение проходит, а более слабое утверждение не проходит - PullRequest
Новая
       92

Дафни: более сильное утверждение проходит, а более слабое утверждение не проходит

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

Первое утверждение говорит, что все значения в массиве missing равны 0. Другой говорит, что как минимум 1 значение в missing равно 0. Если первое утверждение верно, второе также должно быть истинным.

enter image description here

Если кто-то хочет получить полный код, он приводится ниже. По сути, это программа, которая находит пропущенное число в данном массиве. 

method FindMissing(n: int, a: array<int>) returns (m: int)
    requires 2 <= n <= 2 * 100000
    requires a.Length == n - 1
    requires forall j, k :: 0 <= j < k < a.Length ==> a[j] != a[k]
    requires forall k :: 0 <= k < a.Length ==> 1 <= a[k] <= n
    ensures 1 <= m <= n
    ensures forall k :: 0 <= k < a.Length ==> a[k] != m
{
    var missing := new int[n];
    var i := 0;

    while i < missing.Length
        invariant 0 <= i <= missing.Length
        invariant forall k :: 0 <= k < i ==> missing[k] == 0
    {
        missing[i] := 0;
        i := i + 1;
    }

    assert forall k :: 0 <= k < missing.Length ==> missing[k] == 0;

    assert exists k :: 0 <= k < missing.Length && missing[k] == 0;

    i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant forall k :: 0 <= k < i ==> missing[a[k] - 1] == 1
        invariant forall k :: i <= k < a.Length ==> missing[a[k] - 1] == 0
        invariant exists k :: 0 <= k < missing.Length && missing[k] == 0
    {
        missing[a[i] - 1] := 1;
        i := i + 1;
    }

    assert exists k :: 0 <= k < missing.Length && missing[k] == 0;

    i := 0;
    while i < missing.Length {
        if missing[i] == 0 {
            m := i + 1;
            break;
        }
        i := i + 1;
    }
}

1 Ответ

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

Чтобы доказать существование, вам часто нужно предоставить свидетеля. Чтобы сделать это для утверждения, добавьте еще одно утверждение со свидетелем перед ним. Например: 

assert missing[0] == 0;
assert exists k :: 0 <= k < missing.Length && missing[k] == 0;

Для экзистенциального квантификатора в инварианте l oop я предлагаю вам ввести еще одну переменную для хранения свидетеля. Если эта переменная используется только в доказательстве, вы можете сделать ее призраком. Ваш код будет выглядеть примерно так: 

ghost var indexOfMissing := 0;
i := 0;
while i < a.Length
    ...
    invariant 0 <= indexOfMissing < missing.Length && missing[indexOfMissing] == 0

Вам придется вручную обновить indexOfMissing внутри l oop, чтобы сохранить инвариант.

Вот еще один момент о логи c и два замечания о Дафни:

  • Вы начали с того, что forall подразумевает exists. Это не так, если диапазон квантификаторов пуст. К счастью, в вашем случае у вас есть missing.Length != 0.

  • Ваш первый l oop инициализирует элементы от missing до 0. Есть два простых способа сделать это в Дафни. Одним из них является использование агрегатного оператора, который выполняет несколько одновременных присваиваний: 

    forall i | 0 <= i < missing.Length {
  missing[i] := 0;
}

    Другой - дать new функцию, которая говорит, как инициализировать элементы. 

    var missing := new int[n](i => 0);

    Преимущество обоих этих методов в том, что они не являются циклами, а это означает, что вам не нужно поддерживать индекс al oop и записывать различные инварианты l oop.

  • Вы также можете исключить окончательный l oop, если используете оператор присвоения такого: 

    m :| 0 <= m < missing.Length && missing[m] == 0;
...