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
|
ComputerDivision: THEORY
BEGIN
IMPORTING Int
IMPORTING Abs
% do not edit above this line
IMPORTING ints@div, ints@rem
div_total(x: int): int
% Why3 div
div(x:int,
x1:int): MACRO int = IF x1 /= 0 THEN div(x, x1) ELSE div_total(x) ENDIF
% Why3 mod1
mod1(x:int, x1:int): int
mod_total(x: int): int
% Why3 div_mod
div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
y)) + mod1(x, y)))
% Why3 div_bound
div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
((0 <= div(x, y)) AND (div(x, y) <= x))
% Why3 mod_bound
mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
(((-abs(y)) < mod1(x, y)) AND (mod1(x, y) < abs(y)))
% Why3 div_sign_pos
div_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
(div(x, y) >= 0)
% Why3 div_sign_neg
div_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND (y > 0)) =>
(div(x, y) <= 0)
% Why3 mod_sign_pos
mod_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
(mod1(x, y) >= 0)
% Why3 mod_sign_neg
mod_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
(mod1(x, y) <= 0)
% Why3 rounds_toward_zero
rounds_toward_zero: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
(abs((div(x, y) * y)) <= abs(x))
% Why3 div_1
div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
% Why3 mod_1
mod_1: LEMMA FORALL (x:int): (mod1(x, 1) = 0)
% Why3 div_inf
div_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (div(x,
y) = 0)
% Why3 mod_inf
mod_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (mod1(x,
y) = x)
% Why3 div_mult
div_mult: LEMMA FORALL (x:int, y:int, z:int): ((x > 0) AND ((y >= 0) AND
(z >= 0))) => (div(((x * y) + z), x) = (y + div(z, x)))
% Why3 mod_mult
mod_mult: LEMMA FORALL (x:int, y:int, z:int): ((x > 0) AND ((y >= 0) AND
(z >= 0))) => (mod1(((x * y) + z), x) = mod1(z, x))
END ComputerDivision
|
