search

Whiley / WhileyTheoremProver

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.
Apache License 2.0
8 stars 2 forks source link

Problem with Array Update? #43

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following verifies when it should not:

assert:
    forall(int[] arr3, int[] arr2, int[] arr1):
        if:
            arr1 == [1, 2, 4]
            arr2 == arr1
            arr3 == arr2[2:=3]
        then:
            arr3[2] != |arr1|

Observe that replacing arr3 == arr2[2:=3]with arr3 == arr1[2:=3] and it correctly fails.