Floating-point-value-set-parameters
Floating-point value set parameters.
Besides the required support for the float and double value sets,
a Java implementation may provide support for either or both of
a float-extended-exponent value set and
a double-extended-exponent value set
[JLS14:4.2.3].
The support for each extended-exponent value set, if present,
is described by a parameter K [JLS14:4.2.3].
Thus, we parameterize our formal model of Java with an indication,
for each extended-exponent value set,
of whether such a set is supported and, if so, of the value of K.
We introduce two recognizers for the valid values of these parameters
(one for each extended-exponent value set),
and two constrained nullary functions that are the two parameters
and that are required to have values allowed by the recognizers.
Subtopics
- Floatx-paramp
- Recognize the possible parameters that describe
a Java implementation's support of
the float-extended-exponent value set [JLS14:4.2.3].
- Doublex-paramp
- Recognize the possible parameters that describe
a Java implementation's support of
the double-extended-exponent value set [JLS14:4.2.3].
- Floatx-param
- Parameter that describes the support of
the float-extended-exponent value set [JLS14:4.2.3].
- Doublex-param
- Parameter that describes the support of
the double-extended-exponent value set.
