Commit 23382db5 authored by MARCHE Claude's avatar MARCHE Claude

example

parent ee42e57d
......@@ -23,7 +23,7 @@ end
In the following, for each library, we describe the (main) symbols of
each theories defined
\section{Library bool}
\section{Library \texttt{bool}}
\begin{description}
......@@ -34,7 +34,7 @@ each theories defined
\end{description}
\section{Library int}
\section{Library \texttt{int}}
\begin{description}
......@@ -53,7 +53,7 @@ each theories defined
\end{description}
\section{Library real}
\section{Library \texttt{real}}
\begin{description}
......@@ -127,7 +127,7 @@ is inspired from~\cite{ayad10ijcar}.
\end{description}
\section{Library option}
\section{Library \texttt{option}}
\begin{description}
\item[Option] data type \verb|option 'a| with constructors \verb|None| and
......@@ -135,7 +135,7 @@ is inspired from~\cite{ayad10ijcar}.
\end{description}
\section{Library list}
\section{Library \texttt{list}}
\begin{description}
\item[List] data type \verb|list 'a| with constructors \verb|Nil| and
......
theory CosineSingle
use import real.Real
use import real.Abs
use import real.Trigonometry
use import floating_point.Rounding
use import floating_point.Single
(* approximation of cosine function by 1 - x^2 / 2 on interval [-1/32; 1/32] *)
lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
abs (1.0 - x * x * 0.5 - cos x) <= 0x1p-24
(* computation in single precision *)
logic round_single (m:mode) (x:real) : single
axiom RoundSingle: forall m:mode, x:real.
value (round_single m x) = round m x
logic cos_single (x:single) : single =
let x2 = round_single NearestTiesToEven (value x * value x) in
let x2o2 = round_single NearestTiesToEven (0.5 * value x2) in
round_single NearestTiesToEven (1.0 - value x2o2)
lemma TotalError: forall x:single. abs (value x) <= 0x1p-5 ->
let cos_x = cos_single x in
abs (value cos_x - cos (value x)) <= 0x1p-24
end
(*
Local Variables:
compile-command: "../bin/whyide.byte my_cosine.why"
End:
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment