Problem Description

We currently silently truncate rational numbers into integers when doing assignments or pass them as parameters or return values. Currently, the statement Int x = 1/2; is legal and assigns 0 to x.

Proposal

Remove automatic truncation of rational numbers. Attempting to bind a rational value to an identifier of type Int (via variable declaration, assignment, parameter passing, returning a value) shall result in a compile-time type error.

Rationale

Silently truncating values can be surprising and can lead to errors, especially if it occurs in the middle of a larger expression. Auto-conversion, while present in some languages, is not a universal feature.

Cost to implementors

Front end

Implementing this change would mean removing some special-case code from the type checker. Issue 101 will occur for a list of rational numbers with an integer as its first element and will have to be fixed more urgently (but a workaround exists in writing the integer as a rational number with a denominator of 1).

Backends

Implementing this proposed change would result in smaller backends. All backends and their generated models contain code to check for and implement auto-truncation. This code would have to be removed and the changes tested.

Tools

• KeY ABS: simplifies support; favorable to this change.

Cost to users

Existing models that use auto-truncation would no longer type-check and would have to be fixed. The required changes are local to the location of the error and amount to explicitly calling truncate().

Cost of non-adoption

None.