Average Error: 0.2 → 0.2
Time: 1.1m
Precision: 64
\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]
\[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
↓
\[\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \frac{\left(\frac{\left(a + b\right) + c}{2} - b\right) \cdot \left(\frac{\left(a + b\right) + c}{2} + b\right)}{\frac{\left(a + b\right) + c}{2} + b}\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}
↓
\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \frac{\left(\frac{\left(a + b\right) + c}{2} - b\right) \cdot \left(\frac{\left(a + b\right) + c}{2} + b\right)}{\frac{\left(a + b\right) + c}{2} + b}\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r2027955 = a;
        double r2027956 = b;
        double r2027957 = r2027955 + r2027956;
        double r2027958 = c;
        double r2027959 = r2027957 + r2027958;
        double r2027960 = 2.0;
        double r2027961 = /* ERROR: no posit support in C */;
        double r2027962 = r2027959 / r2027961;
        double r2027963 = r2027962 - r2027955;
        double r2027964 = r2027962 * r2027963;
        double r2027965 = r2027962 - r2027956;
        double r2027966 = r2027964 * r2027965;
        double r2027967 = r2027962 - r2027958;
        double r2027968 = r2027966 * r2027967;
        double r2027969 = sqrt(r2027968);
        return r2027969;
}
↓
double f(double a, double b, double c) {
        double r2027970 = a;
        double r2027971 = b;
        double r2027972 = r2027970 + r2027971;
        double r2027973 = c;
        double r2027974 = r2027972 + r2027973;
        double r2027975 = 2.0;
        double r2027976 = r2027974 / r2027975;
        double r2027977 = r2027976 - r2027970;
        double r2027978 = r2027976 * r2027977;
        double r2027979 = r2027976 - r2027971;
        double r2027980 = r2027976 + r2027971;
        double r2027981 = r2027979 * r2027980;
        double r2027982 = r2027981 / r2027980;
        double r2027983 = r2027978 * r2027982;
        double r2027984 = r2027976 - r2027973;
        double r2027985 = r2027983 * r2027984;
        double r2027986 = sqrt(r2027985);
        return r2027986;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 0.2

    \[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  2. Using strategy rm

  3. Applied p16-flip--0.2

    \[\leadsto \sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(b \cdot b\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{b}\right)}\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  4. Simplified0.2

    \[\leadsto \sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\frac{\color{blue}{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{b}\right)\right)}}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{b}\right)}\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  5. Final simplification0.2

    \[\leadsto \sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \frac{\left(\frac{\left(a + b\right) + c}{2} - b\right) \cdot \left(\frac{\left(a + b\right) + c}{2} + b\right)}{\frac{\left(a + b\right) + c}{2} + b}\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]

Reproduce

herbie shell --seed 2019152 
(FPCore (a b c)
  :name "Area of a triangle"
  :pre (and (<.p16 (real->posit16 0) a) (<.p16 (real->posit16 0) b) (<.p16 (real->posit16 0) c))
  (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))