Title :
How to Compute the Area of a Triangle: A Formal Revisit
Abstract :
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, an improvement of its error bound and new investigations in case of underflow.
Keywords :
algorithm theory; floating point arithmetic; theorem proving; Kahan algorithm; algorithm proof; floating-point arithmetic; mathematical value; triangle area; Accuracy; Algorithm design and analysis; Digital arithmetic; Electronic mail; Error analysis; Libraries; Standards; Coq; floating-point arithmetic; formal proof; triangle; underflow;
Conference_Titel :
Computer Arithmetic (ARITH), 2013 21st IEEE Symposium on
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4673-5644-2
DOI :
10.1109/ARITH.2013.29
