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, there is no support for parsing and manipulating functions types. A simple example is:
type fun is (function(int)->(int) p)
assert:
forall(fun f):
f is fun
We need to update the parser, the type system, and probably more. For subtyping we have:
Returns are contra-variant. For example, function()->(int) & function()->(int|null) intersects because int and int|null intersect. However, function()->(int) & function()->(bool) does not intersect because int and bool do not intersect.
Parameters are contra-variant. For example, function(int) & function(int|null) does indeed intersect because !int and !(int|null) intersects. In this case, function()->(int) & function()->(bool) does intersect because !int and !bool do. However, function(int) & function(any) do not.
Currently, there is no support for parsing and manipulating functions types. A simple example is:
type fun is (function(int)->(int) p) assert: forall(fun f): f is funWe need to update the parser, the type system, and probably more. For subtyping we have:
function()->(int) & function()->(int|null)intersects becauseintandint|nullintersect. However,function()->(int) & function()->(bool)does not intersect becauseintandbooldo not intersect.function(int) & function(int|null)does indeed intersect because!intand!(int|null)intersects. In this case,function()->(int) & function()->(bool)does intersect because!intand!booldo. However,function(int) & function(any)do not.