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.
Adding support for bounded quantification would be quite useful. Initially, this could be limited to integer variables only (since this matches Whiley). Possible syntax could be:
assert:
forall(int i in 0..5, int j in 0..10):
if:
i < j
then:
i <= j
There are several key advantages of bounded quantifiers:
The bounds will not trigger quantifier instantiation. Currently, quantifier instantiation restricts itself to trigger only on array accesses. The primary reason for this is that bounds from bounded quantifiers in Whiley otherwise cause lots of needless instantiation. For example, all { i in 0..n | A[i] >= 0} in Whiley current becomes an unbounded quantifier forall(int i).((i >= 0 && i < n) ==> A[i] >= 0)
Finite bounds can be enumerated. In cases where finite bounds are determined, the quantifier can actually be enumerated completely. This saves any potential hassles with quantifier instantiation. Finite bounds do often arise, particularly in the case of array initialisers.
Bounded quantifiers ease model generation. For enumerating models, it turns out to be quite useful to have bounded quantifiers. Basically, this means only the top-level assertion would have unbounded quantification. Thus, for model generation, we only need to range over the top-level quantified variables, rather than all quantified variables.
Adding support for bounded quantification would be quite useful. Initially, this could be limited to integer variables only (since this matches Whiley). Possible syntax could be:
assert: forall(int i in 0..5, int j in 0..10): if: i < j then: i <= jThere are several key advantages of bounded quantifiers:
all { i in 0..n | A[i] >= 0}in Whiley current becomes an unbounded quantifierforall(int i).((i >= 0 && i < n) ==> A[i] >= 0)