examples/numeric/multiplication.mlw

   1 module MultiplicationSingle
   2   use real.RealInfix
   3   use real.Abs
   4   use ufloat.USingle
   5   use ufloat.USingleLemmas
   6
   7   let multiplication_errors_basic (a b c : usingle)
   8     ensures {
   9       let exact = to_real a *. to_real b *. to_real c in
  10       abs (to_real result -. exact) <=.
  11       (2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
  12     }
  13   = a **. b **. c
  14
  15   let multiplication_errors (a b c d e f: usingle)
  16   ensures {
  17     let t = 1.0 +. eps in
  18     let t3 = eps +. (eps *. t) in
  19     let t4 = to_real d *. (to_real e *. to_real f) in
  20     let t5 = (to_real a *. to_real b) *. to_real c in
  21     let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
  22     let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
  23     let exact = t5 *. t4 in
  24     abs (to_real result -. exact) <=.
  25       (* Relative part of the error *)
  26       (eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
  27       (* Absolute part of the error *)
  28       ((t6 +. t6 *. t3) *. abs t5 +.
  29        (t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
  30         *. t +. eta
  31     }
  32   = (a **. b **. c) **. (d **. (e **. f))
  33
  34 end
  35
  36 module MultiplicationDouble
  37   use real.RealInfix
  38   use real.Abs
  39   use ufloat.UDouble
  40   use ufloat.UDoubleLemmas
  41
  42   let multiplication_errors_basic (a b c : udouble)
  43     ensures {
  44       let exact = to_real a *. to_real b *. to_real c in
  45       abs (to_real result -. exact) <=.
  46       (2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
  47     }
  48   = a **. b **. c
  49
  50   let multiplication_errors (a b c d e f: udouble)
  51   ensures {
  52     let t = 1.0 +. eps in
  53     let t3 = eps +. (eps *. t) in
  54     let t4 = to_real d *. (to_real e *. to_real f) in
  55     let t5 = (to_real a *. to_real b) *. to_real c in
  56     let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
  57     let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
  58     let exact = t5 *. t4 in
  59     abs (to_real result -. exact) <=.
  60       (* Relative part of the error *)
  61       (eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
  62       (* Absolute part of the error *)
  63       ((t6 +. t6 *. t3) *. abs t5 +.
  64        (t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
  65         *. t +. eta
  66     }
  67   = (a **. b **. c) **. (d **. (e **. f))
  68 end