mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
55 lines
1.7 KiB
Plaintext
55 lines
1.7 KiB
Plaintext
module AdditionSingle
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.USingle
|
|
use ufloat.USingleLemmas
|
|
|
|
let addition_errors_basic (a b c : usingle) : (r : usingle)
|
|
ensures {
|
|
let exact = to_real a +. to_real b +. to_real c in
|
|
let exact_abs =
|
|
abs (to_real a) +. abs (to_real b) +. abs (to_real c)
|
|
in
|
|
abs (to_real r -. exact) <=. 2. *. eps *. exact_abs
|
|
}
|
|
= a ++. b ++. c
|
|
|
|
|
|
|
|
let addition_errors (a b c d e f : usingle) : (r : usingle)
|
|
ensures {
|
|
let exact = to_real a +. to_real b +. to_real c +. to_real d +.
|
|
to_real e +. to_real f in
|
|
let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) +.
|
|
abs (to_real d) +. abs (to_real e) +. abs (to_real f) in
|
|
abs (to_real r -. exact) <=. 5. *. eps *. exact_abs
|
|
}
|
|
= (a ++. b ++. c) ++. (d ++. (e ++. f))
|
|
end
|
|
|
|
|
|
module AdditionDouble
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.UDouble
|
|
use ufloat.UDoubleLemmas
|
|
|
|
let addition_errors_basic (a b c : udouble)
|
|
ensures {
|
|
let exact = to_real a +. to_real b +. to_real c in
|
|
let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) in
|
|
abs (to_real result -. exact) <=. 2. *. eps *. exact_abs
|
|
}
|
|
= a ++. b ++. c
|
|
|
|
let addition_errors (a b c d e f : udouble)
|
|
ensures {
|
|
let exact = to_real a +. to_real b +. to_real c +. to_real d +.
|
|
to_real e +. to_real f in
|
|
let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) +.
|
|
abs (to_real d) +. abs (to_real e) +. abs (to_real f) in
|
|
abs (to_real result -. exact) <=. 5. *. eps *. exact_abs
|
|
}
|
|
= (a ++. b ++. c) ++. (d ++. (e ++. f))
|
|
end
|