Дафни: Почему это утверждение не работает и как его исправить? - PullRequest
Новая
       49

Дафни: Почему это утверждение не работает и как его исправить?

0 голосов
/ 27 октября 2018

Пытаюсь доказать простой алгоритм на Дафни, но я получаю «нарушение утверждения» на последнем утверждении без дополнительных подробностей. Кто-нибудь может определить, что не так и как это исправить? Формальные методы - не моя специальность. 

method  BubbleSort(a: array?<int>)
    modifies a
    requires a != null
    ensures sorted(a, 0, a.Length -1)
{
    var i := a.Length  - 1;
    while(i > 0)
        decreases i
        invariant i < 0 ==> a.Length == 0
        invariant -1 <= i < a.Length
        invariant sorted(a, i, a.Length -1)
        invariant partitioned(a, i)
    {
        var j := 0;
        while(j < i)
            decreases i - j
            invariant 0 < i < a.Length && 0 <= j <= i
            invariant sorted(a, i, a.Length -1)
            invariant partitioned(a, i)
            invariant forall k :: 0 <= k <= j ==> a[k] <= a[j]
        {
            if(a[j] > a[j+1])
            {
                a[j], a[j+1] := a[j+1], a[j];
            }
            j := j + 1;
        }
        i := i - 1;
    }
}

predicate sorted(a: array?<int>, l: int , u: int)
    reads a //Sintaxe do Dafny. PRECISA disso para dizer que vai ler o array
    requires a != null
{
    forall i, j :: 0 <= l <= i <= j <= u < a.Length ==> a[i] <= a[j]
}

predicate partitioned(a: array?<int>, i: int)
    reads a
    requires a != null
{
    forall k, k' :: 0 <= k <= i < k' < a.Length ==> a[k] <= a[k']
}

method testSort()
{
  var b := new int[2];
  b[0], b[1] := 2, 1;
  assert b[0] == 2 && b[1] == 1;
  BubbleSort(b);
  assert b[0] == 1 && b[1] == 2;
}

1 Ответ

0 голосов
/ 27 октября 2018

Проблема в том, что постусловие (ensures предложение) Sort не дает никакой информации о состоянии A.Когда Dafny выполняет проверку, он проверяет каждый метод независимо, используя только спецификации (не тела) других методов.Поэтому, когда Дафни проверяет testSort, он не смотрит на определение Sort, а только на его постусловие true, которого недостаточно для подтверждения ваших утверждений.

Для получения дополнительной информации см. FAQ и раздел об утверждениях в руководстве .

...