Average Error: 0.2 → 0.2
Time: 52.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(c + b\right) + a}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{2} - a\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(c + b\right) + a}{2} - b\right)\right) \cdot \left(\frac{\left(c + b\right) + a}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r2169829 = a;
        double r2169830 = b;
        double r2169831 = r2169829 + r2169830;
        double r2169832 = c;
        double r2169833 = r2169831 + r2169832;
        double r2169834 = 2.0;
        double r2169835 = /* ERROR: no posit support in C */;
        double r2169836 = r2169833 / r2169835;
        double r2169837 = r2169836 - r2169829;
        double r2169838 = r2169836 * r2169837;
        double r2169839 = r2169836 - r2169830;
        double r2169840 = r2169838 * r2169839;
        double r2169841 = r2169836 - r2169832;
        double r2169842 = r2169840 * r2169841;
        double r2169843 = sqrt(r2169842);
        return r2169843;
}
↓
double f(double a, double b, double c) {
        double r2169844 = a;
        double r2169845 = b;
        double r2169846 = r2169844 + r2169845;
        double r2169847 = c;
        double r2169848 = r2169846 + r2169847;
        double r2169849 = 2.0;
        double r2169850 = r2169848 / r2169849;
        double r2169851 = r2169847 + r2169845;
        double r2169852 = r2169851 + r2169844;
        double r2169853 = r2169852 / r2169849;
        double r2169854 = r2169853 - r2169845;
        double r2169855 = r2169850 * r2169854;
        double r2169856 = r2169853 - r2169844;
        double r2169857 = r2169855 * r2169856;
        double r2169858 = r2169850 - r2169847;
        double r2169859 = r2169857 * r2169858;
        double r2169860 = sqrt(r2169859);
        return r2169860;
}

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(\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right) \cdot \left(\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. Using strategy rm

  5. Applied *p16-rgt-identity-expand0.2

    \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\color{blue}{\left(\left(2\right) \cdot \left(1.0\right)\right)}}\right) \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right) \cdot \left(\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)}\]

  6. Applied *p16-rgt-identity-expand0.2

    \[\leadsto \sqrt{\left(\left(\left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{a}{b}\right)}{c}\right) \cdot \left(1.0\right)\right)}}{\left(\left(2\right) \cdot \left(1.0\right)\right)}\right) \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right) \cdot \left(\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)}\]

  7. Applied p16-times-frac0.2

    \[\leadsto \sqrt{\left(\left(\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(1.0\right)}{\left(1.0\right)}\right)\right)} \cdot \left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right) \cdot \left(\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)}\]

  8. Applied associate-*l*0.2

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

  9. Simplified0.2

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

  11. Applied associate-*r*0.2

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

  12. Final simplification0.2

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

Reproduce

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