## Gallery of proved programs

### Area of a triangle

This function computes the area of a triangle, even if the triangle is needle-like. The algorithm is due to Kahan. The error bound is improved on Goldberg's and overflow and underflow restrictions are given.



/*@ 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)) <= (4.75*0x1p-53 + 33*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))));
}