Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Approximated Cosine in Why3

This is a Why3 version of the Approximated Cosine example


Authors: Claude Marché

Topics: Floating-Point Computations / Non-linear Arithmetic

Tools: Why3 / Gappa / Coq

See also: Approximated Cosine in C annotated in ACSL

index


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