Dafny method will not verify

Question

I have this method that returns the number of trailing zeros, and modifies the array a to replace all the trailing zeros with -1. Currently I am getting assertion might not hold error on assert s == 1 in the validator. Is it something wrong with my invariants or postconditions?

  method modifyArray(a: array<int>) returns (size: nat)
      modifies a
      requires a.Length > 0
      requires forall k :: 0 <= k < a.Length ==> a[k] >= 0
      ensures size <= a.Length
      ensures forall k :: 0 <= k < a.Length - size ==> a[k] == old(a[k])
      ensures forall k :: a.Length - size <= k < a.Length ==> a[k] == -1
      ensures size == a.Length || old(a[a.Length - size - 1]) != 0
    {
      size := 0;
      var i := a.Length - 1;
      while i >= 0 && a[i] == 0
        invariant -1 <= i < a.Length
        invariant size == a.Length - i - 1
        invariant forall k :: i + 1 <= k < a.Length ==> a[k] == -1
        invariant forall k :: 0 <= k <= i ==> a[k] == old(a[k])
        decreases i
      {
        a[i] := -1;
        size := size + 1;
        i := i - 1;
      }
    
    }
    
    method Validate() {
      var a := new int[][0, 42, 0];
      assert a[0] == 0 && a[1] == 42 && a[2] == 0;
      var s := modifyArray(a);
      assert s == 1;  // The tail size should be 1
      assert a[0] == 0 && a[1] == 42 && a[2] == -1;  // The array should have a new tail
    
    }

Answer 1

Your post condition is not strong enough and allows for different (unexpected) implementations. For example, this implementation verifies:

method modifyArray(a: array<int>) returns (size: nat)
  modifies a
  requires a.Length > 0
  requires forall k :: 0 <= k < a.Length ==> a[k] >= 0
  ensures size <= a.Length
  ensures forall k :: 0 <= k < a.Length - size ==> a[k] == old(a[k])
  ensures forall k :: a.Length - size <= k < a.Length ==> a[k] == -1
  ensures size == a.Length || old(a[a.Length - size - 1]) != 0
{
  var i := 0;
  while i < a.Length 
  invariant i <= a.Length 
  invariant forall k :: 0 <= k < i ==> a[k] == -1 {
    a[i] := -1;
    i := i + 1;
  }
  return a.Length;
}

That is not what you are expecting!! To resolve this, I strengthened your postcondition by adding this clause:

ensures forall k :: a.Length - size <= k < a.Length ==> old(a[k]) == 0

This also required an additional loop invariant. With those things in place, the above verified for me.