|
|
|---|
|
|
|
|---|
Abstract placeholders for the Java floating-point values [JLS14:4.2.3], operations [JLS14:4.2.4], and conversions [JLS14:5.1].
Formalizing (Java) floating-point values and their operations is complex. Many interesting Java programs do not use floating-point values; these programs can be formally described by a formal model of Java that does not (yet) include floating-point values. Thus, for now our formal model of Java does not formalize floating-point values and operations.
However, instead of saying something like
`there are no floating-point values',
our model says something like
`there are floating-point values, but we do not know much about them yet'.
This is achieved by introducing weakly constrained ACL2 functions
that recognize floating-point values
and capture operations and conversions on them.
These are analogues of the fully defined recognizers and other functions
over the ACL2 values used to formalize the other (i.e. non-floating-point)
Java primitive values and operations,
such as the recognizer sbyte32p for
Eventually, these weakly constrained ACL2 functions will be replaced with fully defined ones that accurately capture floating-point values, operations, and conversions. This is expected to necessitate minimal (if any) adaptations to the rest of our formal model of Java, because the model already includes (abstract) Java floating-point values. In contrast, if our current model omitted floating-point values altogether, more laborious adaptations would be expected when adding the floating-point values later, e.g. functions defined by cases on the primitive values would have to be extended to cover the newly added cases.