proving correctness of merge sort in dafny

Nov 16, 2015 at 6:33 AM
I learnt dafny recently and I was trying to prove correctness for merge sort but I am facing errors related to loop invariants. Here is link to my dafny implementation - http://rise4fun.com/Dafny/JgOb. Here is a link to same code on pastebin as rise4fun doesn't keep the code around for long time: http://pastebin.com/xZRi8ZzT. I am unable to figure out what's that I am doing wrong. I can't understand why are these invariants failing:

invariant forall x,y:: i <= x <= m && 0 <= y < k < u-l+1 ==> buf[y] <= a[x]
invariant forall x,y:: j <= x <= u && 0 <= y < k < u-l+1 ==> buf[y] <= a[x]
Nov 16, 2015 at 1:30 PM
I think your ms and merge methods need to also say in their post condition that the part of the out array not being sorted is the same as the in array, something like:
ensures forall x :: 0 <= x < l ==> a1[x] == a[x]
ensures forall x :: u < x < a1.Length ==> a1[x] == a[x]
I imagine that you need something similar in the first loop invariant
invariant old(a).Length == a.Length;
invariant forall x :: 0 <= x < a.Length ==> old(a[x]) == a[x];
You will also need to do something similar for the final loop...

Dafny doesn't look inside the loop when verifying the code outside, so you have to tell it what your loop doesn't do as well as what it does do. I think you can put "modifies" clauses on loops too, but I'm not sure this will help much in your example
Marked as answer by deLta30 on 11/16/2015 at 8:38 PM
Nov 16, 2015 at 2:03 PM
Spoiler: here is a verified version http://rise4fun.com/Dafny/TiG7

It uses a modifies clause to simplify the invariants on the loops
k := 0;
while (l+k <= u)
modifies a;
Note that the second to last assertion is important, for some reason I suspect to do with the arithmetic, Dafny doesn't get this by itself.
Marked as answer by deLta30 on 11/16/2015 at 8:38 PM
Nov 16, 2015 at 8:29 PM
Hey,
Thanks for the solution. After looking at all the other posts I was somehow under the impression that it has something to do with triggers. But it turns out that it just needs more specifications.
Can you please elaborate on the need of the second last assert statement?

Thanks again.
Nov 16, 2015 at 9:12 PM
Well, as far as I understand it, the triggers come in when quantifiers are involved. So to prove an assertion with a universal quantifier, we need one or more arbitrary values (with particular properties) to instantiate the quantified variable and continue the proof. In some sense I can think of the proof (at least as far as quantifiers are involved) as trying to make a chain of arbitrary values and matching triggers.

I think this is where that second to last assertion is involved: the way the array index is being calculated in your loop counter/invariant is not matching the trigger for the quantifier in your post condition. Putting in that assertion bridges the gap, matching on the facts provided by the loop invariant on loop exit, and providing a fact that matches the post condition trigger.

By the way, there is some implicit quantification of the whole proof, we are trying to prove "for all initial states that satisfy the precondition, executing the procedure terminates in a state where the postcondition is satisfied" (total correctness).

But, other than the quantifiers, it is also the case that the verification is modular in some ways. There is procedural abstraction at method boundaries, Dafny doesn't look at the body of called procedures when trying to verify the calling procedure. It establishes the pre-condition at the call site, and then assumes the post-condition. Something similar happens at a loop, the body of the loop is abstracted. Dafny proves the invariant at loop entry, and assumes the invariant (and the negation of the loop condition) at loop exit. It modularly also verifies that the loop body maintains the loop invariant, in a similar way that it modularly verifies that called procedures do infact entail their post condition given their precondition.

So the proof of the MergeSort method doesn't involve the body of the ms method. In fact, if you comment out the whole body (including the curly brackets) of the ms method, you can still verify MergeSort - the proof of MergeSort only uses the pre/post conditions of ms not its body. You can do something similar with the loop bodies too.

If you comment out the body of the loops, the method ms will still verify. Although you won't be able to compile and execute it until you fill the loop body in...
 k := 0;
  while (l+k <= u)
  modifies a;
  invariant 0 <= k <= u-l+1
  invariant 0 <= l <= u < a.Length
  invariant k <= buf.Length
  invariant old(a).Length == a.Length;
  invariant forall x :: 0 <= x < l ==> old(a[x]) == a[x];
  invariant forall x :: l+k < x < a.Length ==> old(a[x]) == a[x];
  invariant forall x :: u < x < a1.Length ==> a1[x] == a[x];
  invariant forall x :: 0 <= x < k ==> a[l+x] == buf[x];
  /*{
    a[l + k] := buf[k];
    k := k + 1;
  }*/
Beyond that this all has to do with weakest precondition calculation, and Hoare Logic, if that points you in the right direction.

So, in short its is a bit triggers under the hood, but in your case its more about the way that Dafny goes about verifying loops and procedure calls.
Nov 17, 2015 at 3:47 AM
thanks for the explanation, based on your reply I modified the invariant for the last while loop and it worked - http://rise4fun.com/Dafny/jxIsl . Thanks again for your detailed explanation.