\[\left(\left(1.1102230246251565 \cdot 10^{-16} < a \land a < 9007199254740992\right) \land \left(1.1102230246251565 \cdot 10^{-16} < b \land b < 9007199254740992\right)\right) \land \left(1.1102230246251565 \cdot 10^{-16} < c \land c < 9007199254740992\right)\]
(FPCore (a b c)
:precision binary64
(/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))
↓
(FPCore (a b c)
:precision binary64
(-
(*
0.5
(+
(+
(* (pow c 3.0) (/ (* a a) (/ (pow b 5.0) -4.0)))
(*
(* c c)
(+
(/ a (pow b 3.0))
(* 2.0 (/ (* (/ (* a a) (pow b 4.0)) -1.5) (/ a b))))))
(*
(pow c 4.0)
(+
(/ (* (/ (pow a 4.0) (pow b 8.0)) 2.25) (/ a b))
(* -12.25 (/ (pow a 3.0) (pow b 7.0)))))))
(/ c b)))
double code(double a, double b, double c) {
return (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (-b + sqrt(((b * b) - ((4.0d0 * a) * c)))) / (2.0d0 * a)
end function
↓
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (0.5d0 * ((((c ** 3.0d0) * ((a * a) / ((b ** 5.0d0) / (-4.0d0)))) + ((c * c) * ((a / (b ** 3.0d0)) + (2.0d0 * ((((a * a) / (b ** 4.0d0)) * (-1.5d0)) / (a / b)))))) + ((c ** 4.0d0) * (((((a ** 4.0d0) / (b ** 8.0d0)) * 2.25d0) / (a / b)) + ((-12.25d0) * ((a ** 3.0d0) / (b ** 7.0d0))))))) - (c / b)
end function
public static double code(double a, double b, double c) {
return (-b + Math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
↓
public static double code(double a, double b, double c) {
return (0.5 * (((Math.pow(c, 3.0) * ((a * a) / (Math.pow(b, 5.0) / -4.0))) + ((c * c) * ((a / Math.pow(b, 3.0)) + (2.0 * ((((a * a) / Math.pow(b, 4.0)) * -1.5) / (a / b)))))) + (Math.pow(c, 4.0) * ((((Math.pow(a, 4.0) / Math.pow(b, 8.0)) * 2.25) / (a / b)) + (-12.25 * (Math.pow(a, 3.0) / Math.pow(b, 7.0))))))) - (c / b);
}
def code(a, b, c):
return (-b + math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a)
herbie shell --seed 2023157 -o generate:proofs
(FPCore (a b c)
:name "Quadratic roots, medium range"
:precision binary64
:pre (and (and (and (< 1.1102230246251565e-16 a) (< a 9007199254740992.0)) (and (< 1.1102230246251565e-16 b) (< b 9007199254740992.0))) (and (< 1.1102230246251565e-16 c) (< c 9007199254740992.0)))
(/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))