mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
60 lines
1.3 KiB
Plaintext
60 lines
1.3 KiB
Plaintext
|
|
theory EuclideanDivTest
|
|
|
|
use int.Int
|
|
use int.EuclideanDivision
|
|
|
|
constant div_m1_2 : int = div (-1) 2
|
|
constant mod_m1_2 : int = mod (-1) 2
|
|
constant div_1_m2 : int = div 1 (-2)
|
|
constant mod_1_m2 : int = mod 1 (-2)
|
|
constant div_m1_m2 : int = div (-1) (-2)
|
|
constant mod_m1_m2 : int = mod (-1) (-2)
|
|
|
|
goal ok1 : div_m1_2 = -1
|
|
goal ok2 : mod_m1_2 = 1
|
|
goal ok3 : div_1_m2 = 0
|
|
goal ok4 : mod_1_m2 = 1
|
|
goal ok5 : div_m1_m2 = 1
|
|
goal ok6 : mod_m1_m2 = 1
|
|
|
|
goal smoke1 : div_m1_2 = 0
|
|
goal smoke2 : mod_m1_2 = -1
|
|
goal smoke3 : div_1_m2 = 1
|
|
goal smoke4 : mod_1_m2 = -1
|
|
goal smoke5 : div_m1_m2 = 0
|
|
goal smoke6 : mod_m1_m2 = -1
|
|
|
|
end
|
|
|
|
theory ComputerDivTest
|
|
|
|
use int.Int
|
|
use int.ComputerDivision
|
|
|
|
constant div_m1_2 : int = div (-1) 2
|
|
constant mod_m1_2 : int = mod (-1) 2
|
|
constant div_1_m2 : int = div 1 (-2)
|
|
constant mod_1_m2 : int = mod 1 (-2)
|
|
constant div_m1_m2 : int = div (-1) (-2)
|
|
constant mod_m1_m2 : int = mod (-1) (-2)
|
|
|
|
goal ok1 : div_m1_2 = 0
|
|
goal ok2 : mod_m1_2 = -1
|
|
goal ok3 : div_1_m2 = 0
|
|
goal ok4 : mod_1_m2 = 1
|
|
goal ok5 : div_m1_m2 = 0
|
|
goal ok6 : mod_m1_m2 = -1
|
|
|
|
goal smoke1 : div_m1_2 = -1
|
|
goal smoke2 : mod_m1_2 = 1
|
|
goal smoke3 : div_1_m2 = -1
|
|
goal smoke4 : mod_1_m2 = -1
|
|
goal smoke5 : div_m1_m2 = -1
|
|
goal smoke6 : mod_m1_m2 = 1
|
|
|
|
goal div_pos_neg: forall x y. x>=0 -> y<0 -> div x y <= 0
|
|
|
|
|
|
end
|