Attention Boogie users,
Thanks to Sascha Böhme, Boogie now has support for real numbers. The syntax for integer division/modulus has changed and these operations are now interpreted. The rest of this message describes the full design (which Michal Moskal helped
- Add a new keyword, “real”. It denotes both a built-in type and an int-to-real conversion function.
- Add new keywords “div” and “mod”. They denote integer division and modulus.
- Syntax for real literals. Either of the following:
digit+ '.' digit+ ['e' ['-'] digit+ ]
digit+ 'e' ['-'] digit+
where superfluous leading zeros are okay. The base of the exponent is 10.
New operator overloadings:
- : real --> real
+ : real * real --> real
- : real * real --> real
* : real * real --> real
== : real * real --> bool
!= : real * real --> bool
< : real * real --> bool
<= : real * real --> bool
>= : real * real --> bool
> : real * real --> bool
** : real * real --> real Exponentiation
(which I think is not actually interpreted, but the intention is that it will be when the appropriate SMT support is there). This operator is right-associative, and (despite what its width might suggest) it binds stronger than MulOp's in the grammar
(but weaker than unary operators).
div : int * int --> int (Euclidean division, see
mod : int * int --> int (Euclidean modulus)
/ : int * int --> real
/ : int * real --> real
/ : real * int --> real
/ : real * real --> real
Operators no longer supported:
New built-in functions:
int : real --> int
real : int --> real