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 Type Checking Negation Types #72

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following fails to type check:

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

type neg is (!nat this)

assert "type invariant not satisfied":
    forall(neg x, int&neg y):
        if:
            x > y
        then:
            x >= y

The essential issue is that the type system is reducing int&neg to int&!int which is void.