|
|
|---|
|
|
|
|---|
Abstract placeholders for the Java floating-point values [JLS14:4.2.3].
We introduce constrained recognizers for the float and double value sets, as well as for the float-extended-exponent and double-extended-exponent value sets [JLS14:4.2.3]. The recognizers for the float and double value sets are constrained to be non-empty, via a companion nullary witness function for each, which we also use to define a fixer and a fixtype. The recognizers of the extended-exponent value sets are constrained to be non-empty if and only if the respective value sets are supported, as described by the parameters of our model; their non-emptiness constraints is also expressed via companion nullary witness functions. Since the non-emptiness is conditional (to the parameter's value), we define conditional fixers, but cannot define fixtypes. The nullary witness function for each value sets is regarded as returning the positive 0 for that value set, which is the default value for floating-point variables [JLS14:4.12.5]; this is just reflected in the name of the witness function, not in any constraint property of it.