Wiki Agenda Contact Version française

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

see also the index (by topic, by tool, by reference, by year)


(* Approximated cosine

   Claude Marché (Inria) *)

module M

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

val single_of_real_exact (x: real) : single
  ensures { value result = x }

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

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

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

let my_cosine (x:single) : single
  requires { abs (value x) <=. 0x1p-5 }
  ensures { abs (value result -. cos (value x)) <=. 0x1p-23 }
= 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))

end

download ZIP archive

Why3 Proof Results for Project "my_cosine"

Theory "my_cosine.M": fully verified

ObligationsAlt-Ergo 1.30Coq 8.7.1Gappa 1.3.0MetiTarski 2.4
VC my_cosine------------
split_goal_right
VC my_cosine.0---1.78---0.14
VC my_cosine.10.01---------
VC my_cosine.20.05---------
VC my_cosine.3------0.00---
VC my_cosine.4------0.01---