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 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
|
