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.
The concept of an "assignment" was introduced to reduce the work done in handling equality. However, assignments are a major source of continual problems.
The concept of an "assignment" was introduced to reduce the work done in handling equality. However, assignments are a major source of continual problems.