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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
Single: THEORY
BEGIN
IMPORTING int@Int
IMPORTING real@Real
IMPORTING real@Abs
IMPORTING real@FromInt
IMPORTING Rounding
IMPORTING SingleFormat
% do not edit above this line
% Why3 round
round(x:Rounding.mode, x1:real): real
% Why3 round_logic
round_logic(x:Rounding.mode, x1:real): SingleFormat.single
% Why3 value
value(x:SingleFormat.single): real
% Why3 exact
exact(x:SingleFormat.single): real
% Why3 model
model(x:SingleFormat.single): real
% Why3 round_error
round_error(x:SingleFormat.single): real = abs((value(x) - exact(x)))
% Why3 total_error
total_error(x:SingleFormat.single): real = abs((value(x) - model(x)))
% Why3 no_overflow
no_overflow(m:Rounding.mode, x:real): bool = (abs(round(m,
x)) <= SingleFormat.max_single)
% Why3 bounded_real_no_overflow
bounded_real_no_overflow: LEMMA FORALL (m:Rounding.mode, x:real):
(abs(x) <= SingleFormat.max_single) => no_overflow(m, x)
% Why3 round_monotonic
round_monotonic: LEMMA FORALL (m:Rounding.mode, x:real, y:real):
(x <= y) => (round(m, x) <= round(m, y))
% Why3 round_idempotent
round_idempotent: LEMMA FORALL (m1:Rounding.mode, m2:Rounding.mode,
x:real): (round(m1, round(m2, x)) = round(m2, x))
% Why3 round_value
round_value: LEMMA FORALL (m:Rounding.mode, x:SingleFormat.single):
(round(m, value(x)) = value(x))
% Why3 bounded_value
bounded_value: LEMMA FORALL (x:SingleFormat.single):
(abs(value(x)) <= SingleFormat.max_single)
% Why3 exact_rounding_for_integers
exact_rounding_for_integers: LEMMA FORALL (m:Rounding.mode, i:int):
(((-SingleFormat.max_int) <= i) AND (i <= SingleFormat.max_int)) =>
(round(m, (i :: real)) = (i :: real))
% Why3 round_down_le
round_down_le: LEMMA FORALL (x:real): (round(Rounding.down, x) <= x)
% Why3 round_up_ge
round_up_ge: LEMMA FORALL (x:real): (round(Rounding.up, x) >= x)
% Why3 round_down_neg
round_down_neg: LEMMA FORALL (x:real): (round(Rounding.down,
(-x)) = (-round(Rounding.up, x)))
% Why3 round_up_neg
round_up_neg: LEMMA FORALL (x:real): (round(Rounding.up,
(-x)) = (-round(Rounding.down, x)))
% Why3 of_real_post
of_real_post(m:Rounding.mode, x:real, res:SingleFormat.single): bool =
(value(res) = round(m, x)) AND ((exact(res) = x) AND (model(res) = x))
% Why3 add_post
add_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) + value(y)))) AND ((exact(res) = (exact(x) + exact(y))) AND
(model(res) = (model(x) + model(y))))
% Why3 sub_post
sub_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) - value(y)))) AND ((exact(res) = (exact(x) - exact(y))) AND
(model(res) = (model(x) - model(y))))
% Why3 mul_post
mul_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) * value(y)))) AND ((exact(res) = (exact(x) * exact(y))) AND
(model(res) = (model(x) * model(y))))
% Why3 div_post
div_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
real@Real.infix_sl(value(x), value(y)))) AND
((exact(res) = real@Real.infix_sl(exact(x), exact(y))) AND
(model(res) = real@Real.infix_sl(model(x), model(y))))
% Why3 neg_post
neg_post(x:SingleFormat.single, res:SingleFormat.single): bool =
(value(res) = (-value(x))) AND ((exact(res) = (-exact(x))) AND
(model(res) = (-model(x))))
% Why3 lt
lt(x:SingleFormat.single, y:SingleFormat.single): bool =
(value(x) < value(y))
% Why3 gt
gt(x:SingleFormat.single, y:SingleFormat.single): bool =
(value(x) > value(y))
END Single
|
