A.2.2 Atomic FormulasA.2 ValuesA.2.1 Arithmetic Terms

A.2.1 Arithmetic Terms

Synopsis

Digits
E1+E2
E1-E2
-E1
E1*E2
E1/E2
E1^E2

Descriptions

These expressions represent number literals (composed of the decimal digits 0...9) and the arithmetic operations addition, subtraction, negation, division, and exponentiation. Apart from exponentiation, the types of the values E1 and E2 may be arbitrary (potentially different) arithmetic types (NAT, INT, REAL, range types, and subtypes of arithmetic types). In the case of exponentiation, the type of E1 may be an arbitrary arithmetic type but the type of E2 must be an integral type (NAT, INT, a range type, or a subtype of an integral type).

For determining the result type of each operation, the usual subtype ordering is considered, i.e., NAT and range types are subtypes of INT, and INT is a subtype of REAL. The result type of each function is then the smallest result type that can be deduced from the argument types and the the operation without actually considering the argument values, e.g. adding two NAT values yields a NAT value but adding a NAT value and an INT value yields an INT value. Dividing two values always yields a REAL value. Exponentiation with an exponent E2 of (a subtype of) type NAT yields a result with the type of the base value E1; otherwise the type of the result is REAL.

Pragmatics

For convenience, also the term +E is accepted as a synonym of E.


Wolfgang Schreiner

A.2.2 Atomic FormulasA.2 ValuesA.2.1 Arithmetic Terms