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 Instantiation with Array Updates #79

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following assertion fails:

assert:
    forall(int[] xs, int[] ys):
        if:
            |xs| > 0
            ys == xs[0:=1]
        then:
            exists(int i):
                (0 <= i) && (i < |ys|) && (ys[i] > 0)

The essential problem seems to be that the following quantifier is not being instantiated:

forall(int i).((0 >= (1 + i)) || (i >= |xs|) || (0 >= xs[0:=1][i]))

We can see that this quantifier can, in effect, instantiate itself! Basically with i==0 you have 0 >= 1 giving the contradiction.

DavePearce commented 7 years ago

This might be related to #29.

DavePearce commented 7 years ago

Closing as subsumed by #29.