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
|
class TEST_GCD
--
-- Have a look at feature `gcd' to have an example of
-- assertions in a loop.
-- Also note that SmartEiffel handle recursivity in assertions.
-- (There is also a feature `gcd' in class INTEGER_GENERAL.)
--
creation make
feature
make is
do
check
gcd(3, 4) = 1
gcd(4, 4) = 4
gcd(8, 4) = 4
gcd(9, 8) = 1
gcd(9, 12) = 3
end
end
gcd(value_1, value_2: INTEGER): INTEGER is
-- Great Common Divisor of `value_1' and `value_2'.
require
value_1 > 0; value_2 > 0
local
value: INTEGER
do
from
Result := value_1
value := value_2
invariant
Result > 0
value > 0
gcd(Result, value) = gcd(value_1, value_2)
variant
Result.max(value)
until
Result = value
loop
if Result > value then
Result := Result - value
else
value := value - Result
end
end
ensure
Result = gcd(value_2, value_1)
end
end -- TEST_GCD
|
