Wiki Agenda Contact Version française

Forward error in floating-point computations

These are examples of floating-point programs where we want to automatically generate and prove a post-condition bounding the error between the floating-point computation and the corresponding real computation. They are presented in details in the technical report Generating and Certifying Accuracy Properties of Floating-Point Programs.

Authors: Claude Marché / Paul Bonnot

Topics: Floating-Point Computations / Non-linear Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

download ZIP archive
The following provides the WhyML code where the programs are specified and implemented. After are given the prover results on each verification conditions. 
module AddSubMulSingle
  use real.RealInfix
  use real.Abs
  use ufloat.USingle
  use ufloat.USingleLemmas

  let example1 (a b c d : usingle)
    ensures {
      let exact = (to_real a +. to_real b -. to_real c) *. to_real d in
      let exact_abs = abs ((abs (to_real a +. to_real b) +. abs (to_real c)) *. to_real d) in
      abs (to_real result -. exact) <=. 3.1 *. eps *. exact_abs +. eta
    }
  = (a ++. b --. c) **. d

  let determinant (a b c d : usingle)
    ensures {
      let t1 = to_real a *. to_real d in
      let t2 = to_real b *. to_real c in
      abs (to_real result -. (t1 -. t2))
      <=. 3. *. eps *. (abs t1 +. abs t2) +. 2. *. eta *. (1. +. 2. *. eps)
    }
  = (a **. d --. b **. c)

  let square_norm (a b c : usingle)
    ensures {
      let t1 = to_real a *. to_real a in
      let t2 = to_real b *. to_real b in
      let t3 = to_real c *. to_real c in
      abs (to_real result -. (t1 +. t2 +. t3))
      <=. (5. *. eps) *. (t1 +. t2 +. t3)
           +. eta *.
               (2. *. (1. +. 2. *. eps) *. (1. +. 2. *. eps) +.
                1. +. 4. *. eps)
    }
  = (a **. a ++. b **. b ++. c **. c)

  let example2 (a b c : usingle)
    ensures {
      let t = 1.0 +. eps in
      let t1 = eps +. (eps *. t) in
      let t2 = (to_real a +. to_real b) *. to_real c in
      let t3 = abs t2 in
      let t4 = (t +. t1) *. eta in
      abs (to_real result -. (t2 +. t2))
      <=. ((((t1 +. t1) +. eps) *. (t3 +. t3)) +. (t4 +. t4))
    }
  = ((a ++. b) **. c) ++. ((a ++. b) **. c)
end

module AddSubMulDouble
  use real.RealInfix
  use real.Abs
  use ufloat.UDouble
  use ufloat.UDoubleLemmas

  let example1 (a b c d : udouble)
    ensures {
      let exact = (to_real a +. to_real b -. to_real c) *. to_real d in
      let exact_abs = abs ((abs (to_real a +. to_real b) +. abs (to_real c)) *. to_real d) in
      abs (to_real result -. exact) <=. 3.1 *. eps *. exact_abs +. eta
    }
  = (a ++. b --. c) **. d

  let determinant (a b c d : udouble)
    ensures {
      let t1 = to_real a *. to_real d in
      let t2 = to_real b *. to_real c in
      abs (to_real result -. (t1 -. t2))
      <=. 3. *. eps *. (abs t1 +. abs t2) +. 2. *. eta *. (1. +. 2. *. eps)
    }
  = (a **. d --. b **. c)

  let square_norm (a b c : udouble)
    ensures {
      let t1 = to_real a *. to_real a in
      let t2 = to_real b *. to_real b in
      let t3 = to_real c *. to_real c in
      abs (to_real result -. (t1 +. t2 +. t3))
      <=. (5. *. eps) *. (t1 +. t2 +. t3)
           +. eta *.
               (2. *. (1. +. 2. *. eps) *. (1. +. 2. *. eps) +.
                1. +. 4. *. eps)
    }
  = (a **. a ++. b **. b ++. c **. c)

  let example2 (a b c : udouble)
    ensures {
      let t = 1.0 +. eps in
      let t1 = eps +. (eps *. t) in
      let t2 = (to_real a +. to_real b) *. to_real c in
      let t3 = abs t2 in
      let t4 = (t +. t1) *. eta in
      abs (to_real result -. (t2 +. t2))
      <=. ((((t1 +. t1) +. eps) *. (t3 +. t3)) +. (t4 +. t4))
    }
  = ((a ++. b) **. c) ++. ((a ++. b) **. c)
end
The following table lists all the verification conditions generated and tell which prover proved which.

Why3 Proof Results for Project "add_sub_mul"

Theory "add_sub_mul.AddSubMulSingle": fully verified

ObligationsAlt-Ergo 2.6.0
VC for example1---
split_vc
postcondition---
assert let t = to_real d in let t1 = to_real c in let t2 = abs t in let t3 = 0.0 *. 0.0 in let t4 = eps +. eps in let t5 = 1.0 +. eps in let t6 = to_real a +. to_real b in let t7 = abs t6 +. abs t1 in abs (to_real result -. ((t6 -. t1) *. t)) <=. (((eps +. (((t4 +. 0.0) +. (t4 *. 0.0)) *. t5)) *. (t7 *. t2)) +. ((((((0.0 +. (0.0 *. t4)) *. t7) +. ((0.0 +. t3) *. t2)) +. t3) *. t5) +. eta))
asserted formula---
assert abs (to_real result -. (((to_real a +. to_real b) -. to_real c) *. to_real d)) <=. (((eps +. ((((eps +. eps) +. 0.0) +. ((eps +. eps) *. 0.0)) *. (1.0 +. eps))) *. ((abs (to_real a +. to_real b) +. abs (to_real c)) *. abs (to_real d))) +. ((((((0.0 +. (0.0 *. (eps +. eps))) *. (abs (to_real a +. to_real b) +. abs (to_real c))) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real d))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_single_error_propagation with (a ++. b) --. c,d
apply premises---
assert abs (to_real ((a ++. b) --. c) -. ((to_real a +. to_real b) -. to_real c)) <=. ((((eps +. 0.0) +. eps) *. (abs (to_real a +. to_real b) +. abs (to_real c))) +. ((((1.0 +. eps) +. 0.0) *. 0.0) +. (((1.0 +. eps) +. eps) *. 0.0)))
asserted formula---
apply usub_single_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
asserted formula0.29
postcondition0.62
VC for determinant---
split_vc
postcondition---
assert let t = to_real b *. to_real c in let t1 = to_real a *. to_real d in let t2 = ((1.0 +. eps) +. eps) *. eta in abs (to_real result -. (t1 -. t)) <=. ((((eps +. eps) +. eps) *. (abs t1 +. abs t)) +. (t2 +. t2))
asserted formula---
assert abs (to_real result -. ((to_real a *. to_real d) -. (to_real b *. to_real c))) <=. ((((eps +. eps) +. eps) *. (abs (to_real a *. to_real d) +. abs (to_real b *. to_real c))) +. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta)))
asserted formula---
apply usub_single_error_propagation with a **. d,b **. c
apply premises---
assert abs (to_real (a **. d) -. (to_real a *. to_real d)) <=. ((eps *. abs (to_real a *. to_real d)) +. eta)
asserted formula0.05
apply premises0.02
apply premises---
assert abs (to_real (b **. c) -. (to_real b *. to_real c)) <=. ((eps *. abs (to_real b *. to_real c)) +. eta)
asserted formula0.15
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.01
asserted formula0.03
postcondition0.03
VC for square_norm---
split_vc
postcondition---
assert let t = to_real c in let t1 = to_real b in let t2 = to_real a in let t3 = 1.0 +. eps in let t4 = t *. t in let t5 = t1 *. t1 in let t6 = t2 *. t2 in let t7 = (eps +. eps) +. eps in let t8 = t3 +. eps in let t9 = t8 *. eta in abs (to_real result -. ((t6 +. t5) +. t4)) <=. ((((t7 +. eps) +. eps) *. ((abs t6 +. abs t5) +. abs t4)) +. ((t8 *. (t9 +. t9)) +. ((t3 +. t7) *. eta)))
asserted formula---
assert abs (to_real result -. (((to_real a *. to_real a) +. (to_real b *. to_real b)) +. (to_real c *. to_real c))) <=. ((((((eps +. eps) +. eps) +. eps) +. eps) *. ((abs (to_real a *. to_real a) +. abs (to_real b *. to_real b)) +. abs (to_real c *. to_real c))) +. ((((1.0 +. eps) +. eps) *. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta))) +. (((1.0 +. eps) +. ((eps +. eps) +. eps)) *. eta)))
asserted formula---
apply uadd_single_error_propagation with (a **. a) ++. (b **. b),c **. c
apply premises---
assert abs (to_real ((a **. a) ++. (b **. b)) -. ((to_real a *. to_real a) +. (to_real b *. to_real b))) <=. ((((eps +. eps) +. eps) *. (abs (to_real a *. to_real a) +. abs (to_real b *. to_real b))) +. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta)))
asserted formula---
apply uadd_single_error_propagation with a **. a,b **. b
apply premises---
assert abs (to_real (a **. a) -. (to_real a *. to_real a)) <=. ((eps *. abs (to_real a *. to_real a)) +. eta)
asserted formula0.15
apply premises0.02
apply premises---
assert abs (to_real (b **. b) -. (to_real b *. to_real b)) <=. ((eps *. abs (to_real b *. to_real b)) +. eta)
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
apply premises---
assert abs (to_real (c **. c) -. (to_real c *. to_real c)) <=. ((eps *. abs (to_real c *. to_real c)) +. eta)
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
asserted formula0.03
postcondition0.03
VC for example2---
split_vc
postcondition---
assert let t = 1.0 +. eps in let t1 = eps +. (eps *. t) in let t2 = (to_real a +. to_real b) *. to_real c in let t3 = abs t2 in let t4 = (t +. t1) *. eta in abs (to_real result -. (t2 +. t2)) <=. ((((t1 +. t1) +. eps) *. (t3 +. t3)) +. (t4 +. t4))
asserted formula---
assert abs (to_real result -. (((to_real a +. to_real b) *. to_real c) +. ((to_real a +. to_real b) *. to_real c))) <=. (((((eps +. (eps *. (1.0 +. eps))) +. (eps +. (eps *. (1.0 +. eps)))) +. eps) *. (abs ((to_real a +. to_real b) *. to_real c) +. abs ((to_real a +. to_real b) *. to_real c))) +. ((((1.0 +. eps) +. (eps +. (eps *. (1.0 +. eps)))) *. eta) +. (((1.0 +. eps) +. (eps +. (eps *. (1.0 +. eps)))) *. eta)))
asserted formula---
apply uadd_single_error_propagation with (a ++. b) **. c,(a ++. b) **. c
apply premises---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. abs ((to_real a +. to_real b) *. to_real c)) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. (abs (to_real a +. to_real b) *. abs (to_real c))) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_single_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.05
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
asserted formula0.15
apply premises0.02
apply premises---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. abs ((to_real a +. to_real b) *. to_real c)) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. (abs (to_real a +. to_real b) *. abs (to_real c))) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_single_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.16
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
asserted formula0.03
postcondition0.04

Theory "add_sub_mul.AddSubMulDouble": fully verified

ObligationsAlt-Ergo 2.6.0
VC for example1---
split_vc
postcondition---
assert let t = to_real d in let t1 = to_real c in let t2 = abs t in let t3 = 0.0 *. 0.0 in let t4 = eps +. eps in let t5 = 1.0 +. eps in let t6 = to_real a +. to_real b in let t7 = abs t6 +. abs t1 in abs (to_real result -. ((t6 -. t1) *. t)) <=. (((eps +. (((t4 +. 0.0) +. (t4 *. 0.0)) *. t5)) *. (t7 *. t2)) +. ((((((0.0 +. (0.0 *. t4)) *. t7) +. ((0.0 +. t3) *. t2)) +. t3) *. t5) +. eta))
asserted formula---
assert abs (to_real result -. (((to_real a +. to_real b) -. to_real c) *. to_real d)) <=. (((eps +. ((((eps +. eps) +. 0.0) +. ((eps +. eps) *. 0.0)) *. (1.0 +. eps))) *. ((abs (to_real a +. to_real b) +. abs (to_real c)) *. abs (to_real d))) +. ((((((0.0 +. (0.0 *. (eps +. eps))) *. (abs (to_real a +. to_real b) +. abs (to_real c))) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real d))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_double_error_propagation with (a ++. b) --. c,d
apply premises---
assert abs (to_real ((a ++. b) --. c) -. ((to_real a +. to_real b) -. to_real c)) <=. ((((eps +. 0.0) +. eps) *. (abs (to_real a +. to_real b) +. abs (to_real c))) +. ((((1.0 +. eps) +. 0.0) *. 0.0) +. (((1.0 +. eps) +. eps) *. 0.0)))
asserted formula---
apply usub_double_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.05
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
asserted formula0.31
postcondition0.51
VC for determinant---
split_vc
postcondition---
assert let t = to_real b *. to_real c in let t3 = to_real a *. to_real d in let t4 = ((1.0 +. eps) +. eps) *. eta in abs (to_real result -. (t3 -. t)) <=. ((((eps +. eps) +. eps) *. (abs t3 +. abs t)) +. (t4 +. t4))
asserted formula---
assert abs (to_real result -. ((to_real a *. to_real d) -. (to_real b *. to_real c))) <=. ((((eps +. eps) +. eps) *. (abs (to_real a *. to_real d) +. abs (to_real b *. to_real c))) +. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta)))
asserted formula---
apply usub_double_error_propagation with a **. d,b **. c
apply premises---
assert abs (to_real (a **. d) -. (to_real a *. to_real d)) <=. ((eps *. abs (to_real a *. to_real d)) +. eta)
asserted formula0.15
apply premises0.02
apply premises---
assert abs (to_real (b **. c) -. (to_real b *. to_real c)) <=. ((eps *. abs (to_real b *. to_real c)) +. eta)
asserted formula0.17
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.01
asserted formula0.03
postcondition0.03
VC for square_norm---
split_vc
postcondition---
assert let t = to_real c in let t4 = to_real b in let t5 = to_real a in let t6 = 1.0 +. eps in let t7 = t *. t in let t8 = t4 *. t4 in let t9 = t5 *. t5 in let t10 = (eps +. eps) +. eps in let t11 = t6 +. eps in let t12 = t11 *. eta in abs (to_real result -. ((t9 +. t8) +. t7)) <=. ((((t10 +. eps) +. eps) *. ((abs t9 +. abs t8) +. abs t7)) +. ((t11 *. (t12 +. t12)) +. ((t6 +. t10) *. eta)))
asserted formula---
assert abs (to_real result -. (((to_real a *. to_real a) +. (to_real b *. to_real b)) +. (to_real c *. to_real c))) <=. ((((((eps +. eps) +. eps) +. eps) +. eps) *. ((abs (to_real a *. to_real a) +. abs (to_real b *. to_real b)) +. abs (to_real c *. to_real c))) +. ((((1.0 +. eps) +. eps) *. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta))) +. (((1.0 +. eps) +. ((eps +. eps) +. eps)) *. eta)))
asserted formula---
apply uadd_double_error_propagation with (a **. a) ++. (b **. b),c **. c
apply premises---
assert abs (to_real ((a **. a) ++. (b **. b)) -. ((to_real a *. to_real a) +. (to_real b *. to_real b))) <=. ((((eps +. eps) +. eps) *. (abs (to_real a *. to_real a) +. abs (to_real b *. to_real b))) +. ((((1.0 +. eps) +. eps) *. eta) +. (((1.0 +. eps) +. eps) *. eta)))
asserted formula---
apply uadd_double_error_propagation with a **. a,b **. b
apply premises---
assert abs (to_real (a **. a) -. (to_real a *. to_real a)) <=. ((eps *. abs (to_real a *. to_real a)) +. eta)
asserted formula0.05
apply premises0.02
apply premises---
assert abs (to_real (b **. b) -. (to_real b *. to_real b)) <=. ((eps *. abs (to_real b *. to_real b)) +. eta)
asserted formula0.04
apply premises0.02
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises---
assert abs (to_real (c **. c) -. (to_real c *. to_real c)) <=. ((eps *. abs (to_real c *. to_real c)) +. eta)
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
asserted formula0.03
postcondition0.03
VC for example2---
split_vc
postcondition---
assert let t5 = 1.0 +. eps in let t6 = eps +. (eps *. t5) in let t7 = (to_real a +. to_real b) *. to_real c in let t8 = abs t7 in let t9 = (t5 +. t6) *. eta in abs (to_real result -. (t7 +. t7)) <=. ((((t6 +. t6) +. eps) *. (t8 +. t8)) +. (t9 +. t9))
asserted formula---
assert abs (to_real result -. (((to_real a +. to_real b) *. to_real c) +. ((to_real a +. to_real b) *. to_real c))) <=. (((((eps +. (eps *. (1.0 +. eps))) +. (eps +. (eps *. (1.0 +. eps)))) +. eps) *. (abs ((to_real a +. to_real b) *. to_real c) +. abs ((to_real a +. to_real b) *. to_real c))) +. ((((1.0 +. eps) +. (eps +. (eps *. (1.0 +. eps)))) *. eta) +. (((1.0 +. eps) +. (eps +. (eps *. (1.0 +. eps)))) *. eta)))
asserted formula---
apply uadd_double_error_propagation with (a ++. b) **. c,(a ++. b) **. c
apply premises---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. abs ((to_real a +. to_real b) *. to_real c)) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. (abs (to_real a +. to_real b) *. abs (to_real c))) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_double_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.05
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
asserted formula0.04
apply premises0.02
apply premises---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. abs ((to_real a +. to_real b) *. to_real c)) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
assert abs (to_real ((a ++. b) **. c) -. ((to_real a +. to_real b) *. to_real c)) <=. (((eps +. (((eps +. 0.0) +. (eps *. 0.0)) *. (1.0 +. eps))) *. (abs (to_real a +. to_real b) *. abs (to_real c))) +. ((((((0.0 +. (0.0 *. eps)) *. abs (to_real a +. to_real b)) +. ((0.0 +. (0.0 *. 0.0)) *. abs (to_real c))) +. (0.0 *. 0.0)) *. (1.0 +. eps)) +. eta))
asserted formula---
apply umul_double_error_propagation with a ++. b,c
apply premises---
assert abs (to_real (a ++. b) -. (to_real a +. to_real b)) <=. (eps *. abs (to_real a +. to_real b))
asserted formula0.05
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.01
apply premises0.02
apply premises0.02
asserted formula0.04
apply premises0.02
apply premises0.02
apply premises0.03
apply premises0.01
apply premises0.01
apply premises0.02
apply premises0.02
apply premises0.02
asserted formula0.03
postcondition0.04