Approximated Cosine, exact values and rounding errors
C/ACSL version of the cosine approximated at order 2, specified in terms of exact value and rounding errors
Authors: Claude Marché
Topics: Floating-Point Computations
Tools: Frama-C / Jessie / Gappa / Coq
See also: Approximated Cosine in C annotated in ACSL
see also the index (by topic, by tool, by reference, by year)
Here is the annotated source code
/*@ requires \abs(\exact(x)) <= 0x1p-5; @ requires \round_error(x) <= 0x1p-20; @ ensures \abs(\exact(\result) - \cos(\exact(x))) <= 0x1p-24; @ ensures \round_error(\result) <= \round_error(x) + 0x20081p-41; @*/ float my_cosine2(float x) { float r = 1.0f - x * x * 0.5f; //@ assert \abs(\exact(r) - \cos(\exact(x))) <= 0x1p-24; return r; }
The precondition assumes that the exact value of x is in
[−1/32;1/32], with a rounding error less than 2^{−20}. In the
code, the method error is again stated as an assertion, this time
using the \exact
construct. Then, the postcondition says that,
as before, the exact value of the result is close to the cosine for
not more than 2^{−24}, and the rounding error on the result is
bounded by the original rounding error on x plus
0x20081p-41 (i.e just a bit above 2^{−24}). One may wonder
how this bound was determined: it is indeed possible (although not yet
well instrumented in Frama-C/Jessie) to ask the Gappa tool itself the
most accurate bound. This bound depends on the bound on the rounding
error on x as input. Here is a small table to give in idea on how
these bounds are related: the first line is the bound on the rounding
error on x (times 2^{−20}), whereas the second line is the bound
on the rounding error of the result, minus the one on x (times
2^{−41}).
1 | 2 | 4 | 8 | 16 | 32 |
131201 | 196740 | 327824 | 590016 | 1114496 | 2163840 |
There are 5 VCs generated: 3 VCs for overflow, proved by Gappa, the assertion proved within Coq by the interval tactic, and 2 VCs for the 2 postconditions, both proved by Gappa. The first postcondition on the exact value of the result is also proved by SMT solvers: this is expected since it is a simple consequence of the assertion.
References
- [1]
- Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, Edinburgh, Scotland, July 2010. Springer.
- [2]
- Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 2011.