Reals and Floats

ProB now supports the Atelier-B datatypes REAL and FLOAT. You can turn off this support via the preference ALLOW_REALS.

Standard arithmetic operators can be applied to reals: +, - , *, /, SIGMA, PI. Exponentiation of a real with an integer is also allowed. The comparison predicates =, /=, <, >, <=, >= also all work.

Support for reals and floats is experimental. The definition in Atelier-B is also not stable yet. Currently ProB supports floating point numbers only. Warning: properties such as associativity and commutativity of arithmetic operators thus does not hold.

The library LibraryReals.def in stdlib contains additional useful External Functions (like RSIN, RCOS, RLOG, RSQRT, RPOW, ...).