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.
This should extract the Interpreter.Domain interface and make it a little more general. In particular, by including abstract notions of a Domain.Value. The pretext of this is to enable the interpreter to operate over both concrete and abstract values.
This should extract the
Interpreter.Domaininterface and make it a little more general. In particular, by including abstract notions of aDomain.Value. The pretext of this is to enable the interpreter to operate over both concrete and abstract values.