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

Limitation with ReadableRecordExtractor #107

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The following assertion fails because of some limitation in ReadableRecordExtractor:

type ListAccess is ({Expr index, Expr src} this)
type Expr is (Expr[]|ListAccess this)

assert "type invariant not satisfied":
    forall(!(Expr[])&Expr e):
        if:
            e.src is Expr
        then:
            e.src is Expr

The error message reported is:

./test_type_99.wyal:9: expected record type
            e.src is Expr
            ^

The essential problem is that the following extraction is failing for reasons unknown:

EXTRACTING: ((!((Expr)[])&Expr)&{Expr src, ...}) => null