Boogie now has real, and now interprets integer div/mod

Sep 29, 2012 at 12:51 AM

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 design).

  Rustan

  • 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

New operators:

** :  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 http://en.wikipedia.org/wiki/Modulo_operation)
mod :  int * int --> int    (Euclidean modulus)

Changed operators:

/ :  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

 

Sep 29, 2012 at 10:04 AM

So is it means Dafny will support real numbers natively soon ?

Oct 16, 2012 at 1:24 AM

I admit it would be cool to have a programming language with actual reals, but I don't have them on the forefront of my to-do list.  Would you use them if Dafny supported them?

If Dafny only provides simple arithmetic operations on reals, then the underlying representation at run-time could be rationals--the user would not be able to tell the difference.

Dafny now has support for doing coinductive things--co-inductive datatypes, co-recursive calls, co-predicates, and co-methods.  I just read "CoInduction in Coq" by Yves Bertot, which show a nice example of representing exact reals as infinite streams (of so-called "idigits").  If you wanted to prove that such a representation models the right values, then you would need reals in Dafny.

  Rustan