[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |

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.

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.]]]

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?]]]

[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |

This document was generated by