19. Safe Math Extensions

19.1 \bigint
19.2 \real

The types \bigint and \real are designed to support arbitrary precision arithmetic for integers and floating point numbers. Both types act as primitive value types in JML, with the usual infix arithmetic and logical operations [Chalin04].

However, note that for purposes of Java reflection these types are not actually implemented as primitives. So, since JML equates \TYPE and java.lang.Class, the expression \type(\TYPE).isPrimitive() will return false.

19.1 \bigint

The type \bigint models arbitrary precision integers [Chalin04]. This type is considered by JML to act like a primitive value type, and supports all of the infix arithmetic and logical operators, like int or long. However, note that arithmetic does not wrap around, this for all values i of type \bigint, i < i+1.

Note also that == means value equality for \bigint values, not object identity (even though these values are necessarily represented by objects in a runtime assertion checker). Hence, for example, i+1 == i+2-1 will be true. Similarly != means value inequality, and does not compare object identities.

[[[Needs more discussion and examples.]]]

19.2 \real

The type \real models arbitrary precision floating point numbers [Chalin04]. This type is considered by JML to act like a primitive value type, and supports all of the infix arithmetic and logical operators, like float or double. However, note that arithmetic does not have precision limitations.

Note also that == means value equality for \real values, not object identity (even though these values are necessarily represented by objects in a runtime assertion checker). Hence, for example, i+1 == i+2-1 will be true. Similarly != means value inequality, and does not compare object identities.

[[[Needs more discussion and examples. Is there also a NaN for this type? Are we supposing that it can represent all reals?]]]