Линейный поиск Дафни

При работе над базовым линейным поиском я столкнулся с ошибкой в ​​моем предикате Valid(). Кажется, это работает только тогда, когда я раскомментирую дополнительные операторы гарантии в конструкторе и методе данных. То есть, когда я очень подробно рассказываю о содержании.

У меня также возникают проблемы с постусловием моего поиска, когда элемент не найден.

Любые предложения о том, как решить эту проблему?

  class Search{
    ghost var Contents: set<int>;
    var a : array<int>;

    predicate Valid()
        reads this, a;
    {
        a != null &&
        a.Length > 0 &&

        Contents == set x | 0 <= x < a.Length :: a[x]
    }

    constructor ()
        ensures a != null;
        ensures a.Length == 4;
        //ensures a[0] == 0;
        ensures Valid();
    {
        a := new int[4](_ => 0);
        Contents := {0};
        new;
    }

    method data()
        modifies this, a;
        requires Valid();
        requires a != null;
        requires a.Length == 4;
        ensures a != null;
        ensures a.Length == 4;
        // ensures a[0] == 0;
        // ensures a[1] == 1;
        // ensures a[2] == 2;
        // ensures a[3] == 3;
        ensures Valid();
    {
        a[0] := 0;
        a[1] := 1;
        a[2] := 2;
        a[3] := 3;
        Contents := {0, 1, 2, 3};
    }

    method search(e: int) returns (r: bool)
        modifies this, a;
        requires Valid();
        ensures Valid();
        ensures r == (e in Contents)
        ensures r == exists i: int :: 0 <= i < a.Length && a[i] == e
    {
        var length := a.Length - 1;

        while (length >= 0)
            decreases length;
        {
            var removed := a[length];
            if (e == removed)
            {
                return true;
            }
            length := length - 1;
        }
        return false;
    }
  }


method Main()
{
    var s := new Search();
    s.data();
}

dafny
person DeirdreCleary    schedule 06.11.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Здесь возникает несколько ортогональных проблем.

Во-первых, вы заметили, что Дафни неохотно рассуждает о той части Valid, которая описывает Contents. Это обычная проблема при рассуждениях о множествах в Дафни. По сути, единственный способ, которым Дафни когда-либо «заметит», что что-то является членом множества set x | 0 <= x < a.Length :: a[x], это если оно уже где-то завалялось выражением a[x]. Ваше решение о включении дополнительных постусловий работает, потому что оно упоминает много выражений формы a[x]. Другое решение состоит в том, чтобы включить эти факты в качестве утверждений вместо постусловий:

// in data()
assert a[0] == 0;
assert a[1] == 1;
assert a[2] == 2;
assert a[3] == 3;

Во-вторых, Дафни не может показать, что ваша search процедура удовлетворяет своему постусловию. Вам нужен инвариант цикла, чтобы отслеживать ход поиска. См. руководство для получения дополнительной информации о разработке инвариантов циклов.

В-третьих, Дафни сообщает о проблеме с вашими Main пунктами об изменениях. Вы можете исправить это, добавив постусловие fresh(a) в constructor. Проблема здесь в том, что метод data утверждает, что изменяет a, но Дафни не может сказать, виден ли a вызывающей стороне.

person James Wilcox    schedule 06.11.2017