mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
69 lines
2.1 KiB
Plaintext
69 lines
2.1 KiB
Plaintext
module MultiplicationSingle
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.USingle
|
|
use ufloat.USingleLemmas
|
|
|
|
let multiplication_errors_basic (a b c : usingle)
|
|
ensures {
|
|
let exact = to_real a *. to_real b *. to_real c in
|
|
abs (to_real result -. exact) <=.
|
|
(2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
|
|
}
|
|
= a **. b **. c
|
|
|
|
let multiplication_errors (a b c d e f: usingle)
|
|
ensures {
|
|
let t = 1.0 +. eps in
|
|
let t3 = eps +. (eps *. t) in
|
|
let t4 = to_real d *. (to_real e *. to_real f) in
|
|
let t5 = (to_real a *. to_real b) *. to_real c in
|
|
let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
|
|
let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
|
|
let exact = t5 *. t4 in
|
|
abs (to_real result -. exact) <=.
|
|
(* Relative part of the error *)
|
|
(eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
|
|
(* Absolute part of the error *)
|
|
((t6 +. t6 *. t3) *. abs t5 +.
|
|
(t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
|
|
*. t +. eta
|
|
}
|
|
= (a **. b **. c) **. (d **. (e **. f))
|
|
|
|
end
|
|
|
|
module MultiplicationDouble
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.UDouble
|
|
use ufloat.UDoubleLemmas
|
|
|
|
let multiplication_errors_basic (a b c : udouble)
|
|
ensures {
|
|
let exact = to_real a *. to_real b *. to_real c in
|
|
abs (to_real result -. exact) <=.
|
|
(2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
|
|
}
|
|
= a **. b **. c
|
|
|
|
let multiplication_errors (a b c d e f: udouble)
|
|
ensures {
|
|
let t = 1.0 +. eps in
|
|
let t3 = eps +. (eps *. t) in
|
|
let t4 = to_real d *. (to_real e *. to_real f) in
|
|
let t5 = (to_real a *. to_real b) *. to_real c in
|
|
let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
|
|
let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
|
|
let exact = t5 *. t4 in
|
|
abs (to_real result -. exact) <=.
|
|
(* Relative part of the error *)
|
|
(eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
|
|
(* Absolute part of the error *)
|
|
((t6 +. t6 *. t3) *. abs t5 +.
|
|
(t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
|
|
*. t +. eta
|
|
}
|
|
= (a **. b **. c) **. (d **. (e **. f))
|
|
end
|