The last part of the binary algorithm in chapter 7 suggests to create the NoOverflows invariant. In doing so, the invariant is violated due to high taking MaxInt + 1 value (tested with MaxInt == 7).
The algorithm requires a small fix in the elsif check:
goto Result;
elsif seq[m] < target /\ m < high then
low := m + 1;
else
This allow the model to pass and terminate without causing further overflows.
hwayne
commented
3 years ago
The last part of the binary algorithm in chapter 7 suggests to create the
NoOverflowsinvariant. In doing so, the invariant is violated due tohightakingMaxInt + 1value (tested withMaxInt == 7).The algorithm requires a small fix in the
elsifcheck:This allow the model to pass and terminate without causing further overflows.