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

Quantifier Simplification Problem #71

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following fails to verify:

assert:
    forall(int[] xs, int[] ys, int i, int v):
        if:
            ys == xs[i:=v]
        then:
            contains(ys, v, |ys|)

define contains(int[] xs, int x, int n) is:
    exists(int k):
        (0 <= k) && (k < n) && (xs[k] == x)

The important parts of the generated proof are:

141. nat(i)                                                                    
 129. ys == xs[i:=v]                                                            
 135. |xs| >= (1 + i)                                                           
 160. forall(int k).((v != xs[i:=v][k]) || (0 >= (1 + k)) || (k > (Macro-I 121) 
 161. i >= 0                                                      (Macro-I 141) 
 163. |xs| >= 1                                                 (Ieq-I 135,161)

To get the contradiction, we need to instantiate the quantifier with k => i. But, unfortunately, quantifier instantiation is not being triggered because there is no array access expression xs[i].