Wiki Agenda Contact Version française

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).

12481632
13120119674032782459001611144962163840

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.

See also [1, 2]

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.