# Floating-point-value-placeholders

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.

### Subtopics

- Double-value-abs
- Abstract fixtype for the double value set [JLS14:4.2.3].
- Float-value-abs
- Abstract fixtype for the float value set [JLS14:4.2.3].
- Doublex-value-abs
- Abstract recognizer and fixer
for the double-extended-exponent value set [JLS14:4.2.3].
- Floatx-value-abs
- Abstract recognizer and fixer
for the float-extended-exponent value set [JLS14:4.2.3].