Lack of blanks makes source look confusing
leonardoalt opened this issue · 0 comments
leonardoalt commented
constructor of LValue
interface constructor()
creates
uint x := 0
uint y := 2
invariants
y == 2
behaviour f of LValue
interface f()
storage
x => 0y => 2
This works all the way to prove
, but x => 0y => 2
itself looks a bit confusing to me.
Maybe we should force separators?