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.
At the moment, RecordEqualityCaseAnalysis does not properly support open records. For example, the following should not verify (though currently does):
type Point is ({int x, int y} r)
type OpenPoint is ({int x, int y, ... } r)
assert:
forall(Point p, OpenPoint q):
if:
p == {x: 1, y: 2}
q.x == 1
q.y == 2
then:
p == q
This should not verify because q could have arbitrary many additional fields.
At the moment,
RecordEqualityCaseAnalysisdoes not properly support open records. For example, the following should not verify (though currently does):This should not verify because
qcould have arbitrary many additional fields.