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, macros are declared in WyAL using the define statement as follows:
define greater(int[] xs, int x) is:
forall(int i):
if:
(i >= 0) && (i < |xs|)
then:
xs[i] <= x
However, to be more consistent with Whiley (and to aid integration of the two tools), it would be helpful to use property instead. For example, the above would become:
property greater(int[] xs, int x):
forall(int i):
if:
(i >= 0) && (i < |xs|)
then:
xs[i] <= x
This should be a relatively simple and cosmetic change.
Currently, macros are declared in WyAL using the
definestatement as follows:However, to be more consistent with Whiley (and to aid integration of the two tools), it would be helpful to use
propertyinstead. For example, the above would become:This should be a relatively simple and cosmetic change.