The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata

## Approximated Cosine in Why3

This is a Why3 version of the Approximated Cosine example

Authors: Claude Marché

Tools: Why3 / Gappa / Coq

```module M

use import real.RealInfix
use import real.Abs
use import real.Trigonometry
use import floating_point.Rounding
use import floating_point.Single

val single_of_real_exact : x:real ->
{ }
single
{ value result = x }

val add : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) +. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) +. (value y))}

val sub : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) -. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) -. (value y))}

val mul : x:single -> y:single ->
{ no_overflow NearestTiesToEven ((value x) *. (value y)) }
single
{ value result = round NearestTiesToEven ((value x) *. (value y))}

let my_cosine (x:single) : single =
{ abs (value x) <=. 0x1p-5 }
assert {
abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
};
sub (single_of_real_exact 1.0)
(mul (mul x x) (single_of_real_exact 0.5))
{ abs (value result -. cos (value x)) <=. 0x1p-23 }

end
```