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

Type Checking Recursive Types #113

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The following is generating a StackOverFlowException during type checking:

type Expr is (int|(Expr[]) this)
type Value is (int|(Value[]) this)

assert "type invariant not satisfied":
    forall(int&Expr e):
        e is null|Value

This is clearly related to recursive types in some way.

DavePearce commented 7 years ago

This appears to have been fixed somehow.