CODEWITHSUNDEEP
bubble-sortassertiondafny
ENV
ENV

Reputation: 1282

How to invoke lemma in dafny in bubblesort example?

How to invoke lemma as the reasoning for equality to be true. Consider the following example in dafny where I've created a lemma to say that the sum from 0 to n is n choose 2. Dafny seems to have no problem justifying this lemma. I want to use that lemma to say that the number of swaps in bubblesort has an upper bound of the sum from 0 to n which is equivalent to n choose 2. That being the case, I currently have an error when I try to say it's true by the lemma. Why is this happening and how can I say that equality is true given a lemma?

method BubbleSort(a: array?<int>) returns (n: nat) 
  modifies a
  requires a != null
  ensures n <= (a.Length * (a.Length - 1))/2
{
    var i := a.Length - 1;
    n := 0;
    while (i > 0)
      invariant 0 <= i < a.Length
       {
        var j := 0;
        while (j < i)
          invariant j <= i
          invariant n <= SumRange(i, a.Length)
          {
            if(a[j] > a[j+1])
              {
                a[j], a[j+1] := a[j+1], a[j];
                n := n + 1;
              }
              j := j + 1;
          }
          i := i -1;
      }
    assert n <= SumRange(i, a.Length) == (a.Length * (a.Length - 1))/2 by {SumRangeNChoose2(a.Length)};
    assert n <= (a.Length * (a.Length - 1))/2
}

function SumRange(lo: int, hi: int): int
  decreases hi - lo
{
  if lo == hi then hi
  else if lo >= hi then 0
  else SumRange(lo, hi - 1) + hi
}

lemma SumRangeNChoose2(n: nat)
  ensures SumRange(0, n) == (n * (n - 1))/2
{}

Upvotes: 1

Views: 272

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

You just have a syntax error. There should be no semicolon after the } on the second to last line of BubbleSort. Also, there should be a semicolon after the assertion on the following line.

After you fix the syntax errors, there are several deeper errors in the code about missing invariants, etc. But they can all be fixed using the annotations from my answer to your other question.

Upvotes: 1

Related Questions