Old array reference in Dafny

Question

Why does the assertion in the loop not hold while the assertion before the loop holds?

method m(a: array<int>, m: int)
modifies a;
requires 1 <= m <= a.Length;
{
    var k: int := 1;
    ghost var p_k: int;
    a[(k)-1], k, p_k := a[(k)-1]+1, k+1, k;
    assert old(a[..])[(p_k)-1]+1 == a[(p_k)-1]; 
    while k <= m
    decreases m-k;
    invariant 2 <= k <= m+1;
    invariant 1 <= p_k < k;
    invariant old(a[..])[(p_k)-1]+1 == a[(p_k)-1]; 
    {
        a[(k)-1], k, p_k := a[(k)-1]+1, k+1, k;
        assert old(a[..])[(p_k)-1]+1 == a[(p_k)-1]; 
    }
}

The purpose of the method is solely to understand the behaviour of old and old is used on purpose instead of ghost variables because in the end old is supposed to be used in a post-condition of the method.

Answer 1

I have modified your code so that assert inside loop verifies. See below:

method TestMethod(a: array<int>, m: int)
  modifies a
  requires 0 <=  m < a.Length
{
  var k := 0;
  a[k], k := a[k] + 1, k + 1;
  assert old(a[..])[k-1] + 1 == a[k-1];

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

Reason why assert inside loop is not being verified that before running loop body, dafny doesn't know that old(a[k]) is equal to a[k].