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.
Currently, the WyalFile.Expr API provide concrete nodes for some expressions (e.g. RecordAccess) but only generic nodes for others (e.g. Expr.Operator with OPCODE_arridx). The goal here is to to provide a more unified API.
Currently, the
WyalFile.ExprAPI provide concrete nodes for some expressions (e.g.RecordAccess) but only generic nodes for others (e.g.Expr.OperatorwithOPCODE_arridx). The goal here is to to provide a more unified API.