Average Error: 0.2 → 0.2
Time: 50.9s
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 \left(\frac{\left(a + b\right) + c}{2} - b\right)\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 \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r3756428 = a;
        double r3756429 = b;
        double r3756430 = r3756428 + r3756429;
        double r3756431 = c;
        double r3756432 = r3756430 + r3756431;
        double r3756433 = 2.0;
        double r3756434 = /* ERROR: no posit support in C */;
        double r3756435 = r3756432 / r3756434;
        double r3756436 = r3756435 - r3756428;
        double r3756437 = r3756435 * r3756436;
        double r3756438 = r3756435 - r3756429;
        double r3756439 = r3756437 * r3756438;
        double r3756440 = r3756435 - r3756431;
        double r3756441 = r3756439 * r3756440;
        double r3756442 = sqrt(r3756441);
        return r3756442;
}
↓
double f(double a, double b, double c) {
        double r3756443 = a;
        double r3756444 = b;
        double r3756445 = r3756443 + r3756444;
        double r3756446 = c;
        double r3756447 = r3756445 + r3756446;
        double r3756448 = 2.0;
        double r3756449 = r3756447 / r3756448;
        double r3756450 = r3756449 - r3756443;
        double r3756451 = r3756449 * r3756450;
        double r3756452 = r3756449 - r3756444;
        double r3756453 = r3756451 * r3756452;
        double r3756454 = r3756449 - r3756446;
        double r3756455 = r3756453 * r3756454;
        double r3756456 = sqrt(r3756455);
        return r3756456;
}

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. 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 \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]

Reproduce

herbie shell --seed 2019107 
(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))))