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

(Non-)Empty Type ? #80

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

(this may be related to #77)

The following is failing:

type OpenRecord is ({int x, ...} this)

assert "type invariant not satisfied":
    forall(OpenRecord&!{int x} r):
        if:
            r.x > 0
        then:
            r.x >= 0

The verifier reports empty type for OpenRecord&!{int x}.