mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
50 lines
1.7 KiB
Plaintext
50 lines
1.7 KiB
Plaintext
module SubstractionSingle
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.USingle
|
|
use ufloat.USingleLemmas
|
|
|
|
let substraction_errors_basic (a b c : 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 result -. exact) <=. 2. *. eps *. exact_abs
|
|
}
|
|
= a --. b --. c
|
|
|
|
let substraction_errors (a b c d e f : 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 result -. exact) <=. 5. *. eps *. exact_abs
|
|
}
|
|
= (a --. b --. c) --. (d --. (e --. f))
|
|
end
|
|
|
|
module SubstractionDouble
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.UDouble
|
|
use ufloat.UDoubleLemmas
|
|
|
|
let substraction_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 substraction_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
|