piVC verifies termination when it shouldn't (integer division) #5
Description
I'm preparing a short talk for high school students about program verification, and wanted to use piVC as an approachable example. While writing a binary search implementation, I got into this state, which is verified successfully for both Correctness and Termination, but it doesn't terminate when called as binarySearch([0], 1):
@pre sorted(list, 0, |list|)
@post ((rv = -1 <-> (|list| = 0 || forall i. ((i >= 0 && i < |list|) -> list[i] != target))) && (rv != -1 -> list[rv] = target))
int binarySearch(int[] list, int target) {
if (|list| = 0) return -1;
int first := 0;
int last := |list|;
while @ (sorted(list, 0, |list|) && 0 <= first && first < last && last <= |list|
&& forall i. ((i >= 0 && i < first) -> list[i] < target)
&& forall i. ((i >= last && i < |list|) -> list[i] > target))
# (last - first)
(first != last)
{
int half := (first + last) / 2;
if (list[half] = target)
return half;
if (list[half] > target)
last := half;
else
first := half;
}
if (list[first] = target)
return first;
return -1;
}
I believe the problem is with integer division - for last > first >= 0, (first + last) / 2 > first always holds, but not when we trim the floating point part.