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.
Resolving a name such as
test.f
within the moduletest
currently fails. The reason for this is that there is noimport
statement for the local file!