CODEWITHSUNDEEP
verificationformal-verificationdafny
Vini.g.fer
Vini.g.fer

Reputation: 11909

Dafny: Why is this assertion failing and how to fix it

Trying to prove a simple algorithm on Dafny, but I just get an "assertion violation" on the last assertion with no extra details. Can anybody spot what is wrong and how to fix it? Formal methods is not my specialty.

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;
}

Upvotes: 1

Views: 915

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

The problem is that the postcondition (ensures clause) of Sort gives no information about the state of A. When Dafny does verification, it verifies each method independently, using only the specifications (not the bodies) of other methods. So when Dafny verifies testSort, it doesn't look at the definition of Sort, but only its postcondition true, which isn't enough to prove your assertions.

For more information, see the FAQ and the section on assertions in the tutorial.

Upvotes: 1

Related Questions