search

Whiley / WhileyTheoremProver

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.
Apache License 2.0
8 stars 2 forks source link

Underlying versus Constrained Types #44

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

At the moment, it is impossible to extract the underlying type of a nominal type because of the potential for recursion. This is frustrating as we cannot reduce exactly as we might like. For example:

type nat is (int x) where x >= 0

assert:
   1 is nat

This reduces 1 is nat to (1 is nat) && nat(1). However, it would be preferable to reduce it to (1 is int) && nat(1).

Therefore, one solution might be to introduce a floor operator of the form |_T_|. This operator returns the given type without including its invariant. NOTE: in practice this can be implemented simply as a flag on nominal types.

PROBLEMS: Previously, I have consider such a notation for helping with flow typing:

http://whiley.org/2016/08/03/flow-typing-with-constrained-types/

One of the immediate issues we have to consider is the meaning of floor in the presence of negation types.

DavePearce commented 7 years ago

UPDATE: another option is that we have two type test operators. One only tests the underlying type; the other tests the full type. That actually is the easiest.