Why should the second invariant not hold on entry?

Question

The idea is to reverse an array on site. I have tried with several (recursive) definitions of reverse...getting different behaviors but not the right one...

method arr_reverse (a : array<int>)
modifies a
ensures a[..] == reverse (old(a[..]))

{var i : int, k : int ;

 i, k := 0, a.Length ;
 while k > i + 1
  invariant 0 <= i <= k <= a.Length
  invariant reverse (old(a[..])) == a[..i] + reverse (a[i..k]) + a[k..]
 {
  a[i], a[k-1] := a[k-1], a[i] ;
  i, k := i+1, k-1 ;
 }
}

function reverse (s : seq<int>) : seq<int>
decreases |s|
{if s == [] then s
 else [s[|s|-1]] + reverse (s[..|s|-1])
}

Answer 1

To prove the invariant on entry, you need to give Dafny just one more hint:

assert a[i..k] == a[..];

I found it by trying to prove manually the invariant on entry, by adding several asserts until I found one that make the trick. I'm following the manual to debug verification when verification fails.

When I'm applying this methodology to the body of your while statement, I can write asserts from bottom to top and find this:

  // 6) This was the original invariant. So, between 5 and 6, I just need to prove a result about reverse
  assert reverse (old(a[..])) == a[..i] + reverse (a[i..k]) + a[k..];
  // 5) It might not be easy for Dafny, but we should get to this assert after moving equality
  assert reverse(old(a[..])) == a[..i] + ([a[k-1]] + reverse (a[i+1..k-1]) + [a[i]]) + a[k..];
  // 4) Now I move the assert up again
  assert reverse(old(a[..])) == (a[..i] + [a[k-1]]) + reverse (a[i+1..k-1]) + ([a[i]] + a[k..]);
  a[i], a[k-1] := a[k-1], a[i] ;
  // 3) I do a bit of guessing to make "a[i]" and "a[k-1]" to appear
  assert reverse(old(a[..])) == (a[..i] + [a[i]]) + reverse (a[i+1..k-1]) + ([a[k-1]] + a[k..]);
  // 2) I use verification debugging to "move the assert up"
  assert reverse(old(a[..])) == a[..i+1] + reverse (a[i+1..k-1]) + a[k-1..];
  i, k := i+1, k-1 ;
  // 1) I write the invariant
  assert reverse(old(a[..])) == a[..i] + reverse (a[i..k]) + a[k..];

So the only thing that remain (besides maybe other lemmas of associativity you might have to invoke), is to prove the non-trivial lemma that reverse (a[i..k]) == [a[k-1]] + reverse (a[i+1..k-1]) + [a[i]]