The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
The following Whiley code fails verification when called from WyC, but not when the generated WyAL is verified directly:
type expr is int[] | bool
function cons(int item, int[] input) -> int[]:
int[] result = [0; |input|+1]
int i = 0
//
while i < |input|
where i >= 0
where |result| == |input|+1:
//
result[i+1] = input[i]
i = i + 1
//
result[0] = item
return result
The error message reported is:
./TypeEquals_Valid_32.whiley:14: index out of bounds (not less than length)
result[0] = item
^^^^^^^^^
Observe that adding |input| >= 0 to the loop invariant and all is well.
DavePearce
commented
7 years ago
The following Whiley code fails verification when called from WyC, but not when the generated WyAL is verified directly:
The error message reported is:
Observe that adding
|input| >= 0to the loop invariant and all is well.