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 Reasoning about Type Tests #17

Closed DavePearce closed 7 years ago

DavePearce commented 8 years ago

The following assertion fails:

assert:
    forall (null | int x):
        if:
            x is !(int)
        then:
            x is null

The reason is that it reduces down to this automaton:

Exists[{[Var("r0"),OrT{IntT,NullT}]},And{
    Is[Var("r0"),NotT(IntT)],
    Not(Is[Var("r0"),NullT])
}]

In order to get the final contradiction, it needs to intersect with the type of variable itself.

DavePearce commented 7 years ago

Replaced by #30