1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
module AdditionSingle
use real.RealInfix
use real.Abs
use ufloat.USingle
use ufloat.USingleLemmas
let addition_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 addition_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 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
|
