Trying to Prove MergeSort in Dafny & Receiving an Error on Post Condition of Merge Method

Hello fellow Dafny enjoyers,

I am learning/using Dafny for a college group project and experiencing a problem in my MergeSort implementation. From what I understand I'm having a difficult time understanding how to use invariants to solve my postcondition error. Below is the code of my Merge method:

method Merge(left: seq<int>, right: seq<int>) returns (merged: seq<int>)
    // Pre-Conditions: denoted by requires
    requires sorted(left) && sorted(right)

    // Post-Conditions: denoted by ensures
    ensures sorted(merged)
    ensures |merged| == |left| + |right|
{
    // 1. Initialize Variables
    var i := 0;
    var j := 0;
    merged := [];

    // 2. Create the merge logic
    while i < |left| && j < |right|
        invariant 0 <= i <= |left|
        invariant 0 <= j <= |right|
        invariant |merged| == i + j
    {
        if left[i] < right[j] {
            merged := merged + [left[i]];
            i := i + 1;
        } else {
            merged := merged + [right[j]];
            j := j + 1;
        }
    }
        
    // 3. Consider left-over elements
    if i < |left| {
        merged := merged + left[i..];
    }
    if j < |right| {
        merged := merged + right[j..];
    }
    
    return merged;
}

This method also uses this predicate to check if the sequence is in sorted order:

predicate sorted(s: seq<int>)
{
  forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

The error stems from the ensures sorted(merged) line which then makes our predicate unsolvable.

What we've tried so far:

Working backwards through the algorithm to try and find/use invariants to help Dafny prove our algorithm
Testing the algorithm to make sure it works correctly (hint: it does 😊)
Trying to use assertions to help Dafny get closer to proving our algorithm

Error happening in particular.

Solution

Glad that you tried out a lot of things. To avoid shooting arrows in the dark and come up with an invariant out of thin air, there is a way to fix verification (or find counter-examples) systematically using verification debugging techniques.

Here is how it would work in your case.

Add assert sorted(merged); just before the last return. Now the error is captured by this assertion, and the postcondition verifies

    if j < |right| {
        merged := merged + right[j..];
    }
    assert sorted(merged); // Fails now
    return merged;         // Verifies

Copy and paste assert sorted(merged); both above the if, and below the single assignment merged := merged + right[j..];of the if, following the if-rule in verification debugging. The previous assertion now verifies, and now you have two assertions that fail.

    assert sorted(merged);     // Fails now
    if j < |right| {
        merged := merged + right[j..];
        assert sorted(merged); // Fails now
    }
    assert sorted(merged);     // Verifies
    return merged;

Move the second assert above the assignment by applying weakest precondition rules for assignment (again in the table of verification debugging)

assert sorted(merged); if j < |right| { assert sorted(merged + right[j..]); // fails merged := merged + right[j..]; assert sorted(merged); // Now verifies } assert sorted(merged); return merged;
Move the inner assert before the if statement by applying weakest precondition rules for the if (also in the table of verification debugging)

assert sorted(merged); assert j < |right| ==> sorted(merged + right[j..]); // fails if j < |right| { assert sorted(merged + right[j..]); // Now verifies merged := merged + right[j..]; assert sorted(merged); }
At this point, you should step back a bit: how do you prove that a concatenation is sorted? How do you know? if you had to write a lemma, what would be the necessary hypotheses? I leave it to you as an exercise.
Once you have locally realized what it will mean to prove everything, you will have a few asserts just after the while loop. Now is the time to generalize them to transform them to invariants. Sometimes it's obvious, sometimes it's not. In your case, the invariant should remember something about the sortedness of merge and the elements it contains compared to left and right.

Let me know how it goes!