Commit 118e150e authored by MARCHE Claude's avatar MARCHE Claude

new example in progress: approximation of exponential

parent 8a90c2ca
/**************************************************************************/
/* */
/* The Why platform for program certification */
/* */
/* Copyright (C) 2002-2017 */
/* */
/* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud */
/* Claude MARCHE, INRIA & Univ. Paris-sud */
/* Yannick MOY, Univ. Paris-sud */
/* Romain BARDOU, Univ. Paris-sud */
/* */
/* Secondary contributors: */
/* */
/* Thierry HUBERT, Univ. Paris-sud (former Caduceus front-end) */
/* Nicolas ROUSSET, Univ. Paris-sud (on Jessie & Krakatoa) */
/* Ali AYAD, CNRS & CEA Saclay (floating-point support) */
/* Sylvie BOLDO, INRIA (floating-point support) */
/* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) */
/* Mehdi DOGGUY, Univ. Paris-sud (Why GUI) */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Lesser General Public */
/* License version 2.1, with the special exception on linking */
/* described in file LICENSE. */
/* */
/* This software is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */
/**************************************************************************/
/*@ requires \abs(x) <= 1.0;
@ ensures \abs(\result - \exp(x)) <= 0x1p-4; */
double my_exp(double x) {
/*@ assert \abs(0.9890365552 + 1.130258690*x +
@ 0.5540440796*x*x - \exp(x)) <= 0x0.FFFFp-4; */
return 0.9890365552 + 1.130258690 * x + 0.5540440796 * x * x;
}
/*
Local Variables:
compile-command: "make exp.why3ide"
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