Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit c579bbba authored by Sylvain Dailler's avatar Sylvain Dailler

Converted examples from C to why3

parent 9ccc3cd0
/**************************************************************************/
/* */
/* 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;
}
module Exp
use import ieee_float.Float64
use import real.Abs
use import real.ExpLog
use import real.Real
let my_exp (x: t) : t
requires {abs (t'real x) <= 1.0}
ensures { abs (t'real result - exp (t'real x)) <= 0x1p-4} (* 1 * 2 ^ - 4 *)
=
assert {
let x = t'real x in
abs(0.9890365552 + 1.130258690*x +
0.5540440796*x*x - exp(x)) <= 0x0.FFFFp-4};
(0x1.FA62FFD643D6Ep-1:t) .+ (0x1.2158A22D91DE9p0:t) .* x .+
(0x1.1BABAA64D94DBp-1:t) .* x .* x
/*
Local Variables:
compile-command: "make exp.why3ide"
End:
*/
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