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.
Having now implemented open records, an interesting question arises. Should the following hold or not?
type OpenPoint is ({int x,int y, ...} p)
assert:
forall(OpenPoint p):
if:
p.z > 0
then:
p.z >= 0
The argumentation here is that, since p.z > 0 is an assumption, it follows that the type of p can be inferred as at least {int x, int y, int z, ...}. This would presumably be implementing using an axiom of some kind. However, I don't really know how the type checker should or could handle this.
Having now implemented open records, an interesting question arises. Should the following hold or not?
type OpenPoint is ({int x,int y, ...} p) assert: forall(OpenPoint p): if: p.z > 0 then: p.z >= 0The argumentation here is that, since
p.z > 0is an assumption, it follows that the type ofpcan be inferred as at least{int x, int y, int z, ...}. This would presumably be implementing using an axiom of some kind. However, I don't really know how the type checker should or could handle this.