CODEWITHSUNDEEP
dafny
mackmut
mackmut

Reputation: 23

Sorted post-condition doesn't hold

What I want to do in the method is simply to overwrite the previous array and fill it with number that are sorted, however dafny says that the post-condition does not hold and I can't for the life of me figure out why. I'm guessing I need to add some invariant to the loop but since they are checked before entering the loop I don't know how to put a valid invariant.

method sort2(a : array<int>)
modifies a;
requires a != null && a.Length >= 2;
ensures sorted2(a[..]);
{
  var i := a.Length - 1;
  while (i >= 0)
  decreases i
 {
     a[i] := i;
     i := i - 1;
 }
}

predicate sorted2(s: seq<int>)
{
    forall i :: 1 <= i < |s| ==> s[i] >= s[i-1]
}

My previous attempt was just to reinitialize a but dafny apparently doesn't allow that inside methods.

Upvotes: 1

Views: 320

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

You do need a loop invariant in order to prove this program correct.

See Section 6 of the Dafny Tutorial for a general introduction to loop invariants and how to come up with them.

In this case, a good loop invariant will be something like sorted(a[i+1..]), which says that the part of the array after index i is sorted. That way, when the loop terminates and i is zero, you'll know that the whole array is sorted.

You will also need one or two more loop invariants describing bounds on i and the elements of the array itself.

Upvotes: 1

Related Questions