Skip to content
Snippets Groups Projects
Commit ed2fe1ee authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

[doc] Clarified ieee 754 floating point requirement in spec

parent f79bbbbc
No related branches found
No related tags found
No related merge requests found
...@@ -125,11 +125,15 @@ our theory ``ACASXU_P1``. ...@@ -125,11 +125,15 @@ our theory ``ACASXU_P1``.
We will need to write down some numerical values. As of now, CAISAR allows We will need to write down some numerical values. As of now, CAISAR allows
writing values using floating-point arithmetic only. Why3 defines a float type writing values using floating-point arithmetic only. Why3 defines a float type
and the relevant arithmetic operations according to the IEEE floating-point and the relevant arithmetic operations according to the IEEE 754 floating-point
standard in a theory, astutely called ``ieee_float``. Specifically, we will standard in a theory, astutely called ``ieee_float``. Specifically, we will
import the ``Float64`` sub-theory, that defines everything we need for 64-bit import the ``Float64`` sub-theory, that defines everything we need for 64-bit
precision floating-point numbers. We thus import it in our theory using the precision floating-point numbers. We thus import it in our theory using the
``use`` keyword. ``use`` keyword.
This currently requires to write exact IEEE 754 floating
point values in the specification file, which is
understandably a setback in terms of usability, but have the
advantage of being unambiguous on the specification.
Our file looks like this so far: Our file looks like this so far:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment