Area of a triangle
How to accurately compute the area of a triangle.
Auteurs: Sylvie Boldo
Catégories: Floating-Point Computations / Arithmetic
Outils: Frama-C / Jessie / Why3 / Coq
see also the index (by topic, by tool, by reference, by year)
This programs computes the area of a triangle given its side lengths. When the triangle is needle-like, the common formula has a very poor accuracy. Kahan proposed in 1986 an algorithm he claimed correct within a few ulps. Goldberg took over this algorithm in 1991 and gave a precise error bound. This program is formally proved with an improvement of its error bound and new investigations in case of underflow.
/*@ requires 0 <= x;
@ ensures \result==\round_double(\NearestEven,\sqrt(x));
@*/
double sqrt(double x);
/*@ logic real S(real a, real b, real c) =
@ \let s = (a+b+c)/2;
@ \sqrt(s*(s-a)*(s-b)*(s-c));
@ */
/*@ requires 0 <= c <= b <= a && a <= b + c && a <= 0x1p255;
@ ensures 0x1p-513 < \result
@ ==> \abs(\result-S(a,b,c)) <= (53./8*0x1p-53 + 29*0x1p-106)*S(a,b,c);
@ */
double triangle (double a,double b, double c) {
return (0x1p-2*sqrt((a+(b+c))*(a+(b-c))*(c+(a-b))*(c-(a-b))));
}