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.
type nat is (int x) where x >= 0
type pos is (int x) where x > 0
assert:
forall (int x):
if:
x is nat
then:
x is pos
The key problem is that TypeTestClosure reduces this to x is (nat&!pos) (effectively x is (int&!int)) which clearly gives a contradiction. But, of course, this is ignoring the constraints involved.
The problem essentially boils down to this segment:
Type intersection = new Type.Intersection(lhsT,rhsT);
//
if (types.isRawSubtype(new Type.Void(), intersection)) {
// No possible intersection exists between the types in
// question. Therefore, the test cannot be true.
return state.subsume(this, typeTest, state.allocate(new Formula.Truth(false)));
}
Basically, it's not true in the case of constrained types that isRawSubtype determines categorically that there is no intersection between the two types. For example, consider nat :> pos which corresponds to int :> int as a raw subtype test (which is clearly incorrect).
How do we handle this properly? The test nat :> pos translates to the void test (!nat) & pos. To determine the type really is equivalent to void, we want to compute ⌈(!nat)&pos⌉ which expands to (!⌊nat⌋)&⌈pos⌉ and then (!void)&int (which does not return true).
The following verifies when it clearly shouldn't:
The key problem is that
TypeTestClosure
reduces this tox is (nat&!pos)
(effectivelyx is (int&!int)
) which clearly gives a contradiction. But, of course, this is ignoring the constraints involved.The problem essentially boils down to this segment:
Basically, it's not true in the case of constrained types that
isRawSubtype
determines categorically that there is no intersection between the two types. For example, considernat :> pos
which corresponds toint :> int
as a raw subtype test (which is clearly incorrect).How do we handle this properly? The test
nat :> pos
translates to the void test(!nat) & pos
. To determine the type really is equivalent to void, we want to compute⌈(!nat)&pos⌉
which expands to(!⌊nat⌋)&⌈pos⌉
and then(!void)&int
(which does not return true).