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.
type state is ({int x, int y} this)
type pState is (state this)
assert "assertion failed":
forall(pState p1, pState p2):
if:
*p2 == (*p1){x:=0}
then:
(*p2).x == 0
The reported error is:
./test.wyal:7: unknown type encountered
*p2 == (*p1){x:=0}
^
This must be related to code for parsing casts. To resolve this we need to add some kind of lookahead function, or use an alternative mechanism for casts.
(this is related to #100)
The following fails to parse:
The reported error is:
This must be related to code for parsing casts. To resolve this we need to add some kind of lookahead function, or use an alternative mechanism for casts.