Average Error: 0.2 → 0.2
Time: 43.4s
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{a + \left(b + c\right)}{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{a + \left(b + c\right)}{2} - c\right)}
double f(double a, double b, double c) {
        double r4562487 = a;
        double r4562488 = b;
        double r4562489 = r4562487 + r4562488;
        double r4562490 = c;
        double r4562491 = r4562489 + r4562490;
        double r4562492 = 2.0;
        double r4562493 = /* ERROR: no posit support in C */;
        double r4562494 = r4562491 / r4562493;
        double r4562495 = r4562494 - r4562487;
        double r4562496 = r4562494 * r4562495;
        double r4562497 = r4562494 - r4562488;
        double r4562498 = r4562496 * r4562497;
        double r4562499 = r4562494 - r4562490;
        double r4562500 = r4562498 * r4562499;
        double r4562501 = sqrt(r4562500);
        return r4562501;
}
↓
double f(double a, double b, double c) {
        double r4562502 = a;
        double r4562503 = b;
        double r4562504 = r4562502 + r4562503;
        double r4562505 = c;
        double r4562506 = r4562504 + r4562505;
        double r4562507 = 2.0;
        double r4562508 = r4562506 / r4562507;
        double r4562509 = r4562508 - r4562502;
        double r4562510 = r4562508 * r4562509;
        double r4562511 = r4562508 - r4562503;
        double r4562512 = r4562510 * r4562511;
        double r4562513 = r4562503 + r4562505;
        double r4562514 = r4562502 + r4562513;
        double r4562515 = r4562514 / r4562507;
        double r4562516 = r4562515 - r4562505;
        double r4562517 = r4562512 * r4562516;
        double r4562518 = sqrt(r4562517);
        return r4562518;
}

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

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

Reproduce

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