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

Precedence for Parsing Unary Operators #100

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

The intention with WyAL is that there is no operator precedence. And yet, at this time, the following assertion is parsed:

type Point is ({int x, int y} this)

assert "assertion failed":
    forall(&test.Point p):
        if:
            *p.x == 0
        then:
            *p.x == 0

This results in the following type error:

./test.wyal:6: expected record type
            *p.x == 0
             ^

However, it should clear report something like ambiguous expression encountered (braces required).

DavePearce commented 7 years ago

Have added the following test case which currently parses and verified, but should not:

type Point is ({&int x, int y} this)

assert "assertion failed":
    forall(test.Point p):
        if:
            0 == *p.x
        then:
            0 == *p.x