DOUBLE_REF

Used .NET classes

• CONVERT
• MATH

Static methods used

• {MATH}.floor, ceiling, abs_double
• {CONVERT}.to_int32, to_string_double

Security notes

• None.

Unhandled exceptions

• When converting double's into integer's (round, ceiling, floor, truncated_to_integer), an exception might be raised if the result is larger than the larger integer available, or smaller than the smallest integer available.

Other notes

The implementation of some features seems to be very slow (round for example). That's because of the strong postcondition.