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

Multi-Variable Quantifier Instantiation #126

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following fails to verify for reasons unknown:

type nat is (int x)
where:
    x >= 0

type Digraph is ((nat[])[] edges)
where:
    forall(int i, int j):
        if:
            (0 <= i) && (i < |edges|)
            (0 <= j) && (j < |edges[i]|)
        then:
            edges[i][j] < |edges|

assert "type invariant not satisfied":
    forall(Digraph g):
        g is Digraph

It's possible that the reason is related to the use of a multi-variable quantifier.

DavePearce commented 7 years ago

UPDATE. Removing the nat requirement and this does indeed verify.