mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
76 lines
2.0 KiB
Plaintext
76 lines
2.0 KiB
Plaintext
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
|
|
|