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

Split SubtypeOperator into Two Forms #64

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

There is a problem with the meaning of SubtypeOperator.isSubtype(). Specifically, there are really three cases it should handle:

  1. Definite Subtype. For example, int|null :> int is definitely true.
  2. Definite Non-Subtype. For example, int :> int|null is definitely false.
  3. Unknown. For example, nat :> pos is unknown. More specifically, whilst the underlying or raw types are subtypes (i.e. int :> int), we cannot be so sure about the actual types because of their type invariants. That is, we cannot reason within the type checker that the invariant for nat implies that for pos.

At the moment, the subtype operator only provides binary information and, hence, cannot describe the third case.

DavePearce commented 7 years ago

This is now done, though it's pretty clear that I don't know how to properly implement an instance of SubtypeOperator at this time.

DavePearce commented 7 years ago

See #65 for potential solution. Apparently, I do know since the WhileyCompiler already solves this problem :)