Chained relational expressions are not parsed correctly.

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)

GNU General Public License v3.0

4 stars 0 forks source link

Chained relational expressions are not parsed correctly. #176

Closed mattulbrich closed 4 years ago

mattulbrich commented 4 years ago

The following should be parsable in Dafny, but are not all in DIVE:

lemma m(x: int, y:int, z:int)

[x] requires x == y == z
[x] requires x > y > z
[x] requires x > y == z
[x] requires x == y >= z
[x] requires (x > 0) == true
[x] requires (x == 0) == true

{}

SpringVaS commented 4 years ago

Why is here the required keyword used, rather than ensures?

mattulbrich commented 4 years ago

Because it does not matter. The term x>y>z must be digested by the parser and it is irrelevant in what context. Hence, requires is as good as ensures or any other construct.

SpringVaS commented 4 years ago

I see. requires does not load the lemma as a rule in DIVE, though. But that has nothing to do with this issue, so I was confused.