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
}
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.