How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound

Sylvie Boldo (1, 2)

1 LRI - Laboratoire de Recherche en Informatique
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

Mathematical values are usually computed using well-known mathematical formulas without thinking about their accuracy, which may turn awful with particular instances. This is the case for the computation of the area of a triangle. 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 article presents a formal proof of this algorithm, investigations in case of underflow and a new improvement of its error bound.

Domaines: Logique en informatique [cs.LO]

Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound. 2013. ⟨hal-00862653⟩