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

Array Access with Negative Index? #132

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following verifies which it shouldn't really:

assert:
    forall(int[] items, int item, int i, int i$3):
        if:
            i == 0
            0 >= |items|
        then:
            items[-1] == item

The generated proof is:

 49. exists(int[] items, int item, int i, int i$3).((((i == 0) && ((0 + 1) > () 
 56. exists(int[] items, int item, int i, int i$3).((i == 0) && (0 >= (Simp 49) 
 55. (i == 0) && (0 >= |items|) && (item != items[-1])            (Exists-E 56) 
 50. 0 >= |items|                                                    (And-E 55) 
 54. item != items[-1]                                               (And-E 55) 
 57. |items| >= 0                                                 (ArrLen-I 50) 
 38. false                                                     (ArrIdx-I 57,54)

The problem is presumably that -1 >= 0 is being generated by ArrIdx-I ... ?

Hmmmm, maybe this isn't a problem since we are assuming that the formula is well-formed? That is, the invalid array access should be caught elsewhere?