GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
tutorial
>
TOWER
+
Point of view
All features
ANY
HANOI
All features
class TOWER
Summary
top
Direct parents
Insert list:
ANY
Overview
top
Creation features
{
ANY
}
full
(n:
INTEGER_32
)
empty
(n:
INTEGER_32
)
Features
{}
t
:
ARRAY
[
INTEGER_32
]
top
:
INTEGER_32
{}
full
(n:
INTEGER_32
)
empty
(n:
INTEGER_32
)
{
HANOI
}
nb
:
INTEGER_32
show_a_discus
(d:
INTEGER_32
, picture:
STRING
)
remove_discus
:
INTEGER_32
add_discus
(d:
INTEGER_32
)
t
:
ARRAY
[
INTEGER_32
]
writable attribute
{}
top
top
:
INTEGER_32
writable attribute
{}
top
full
(n:
INTEGER_32
)
effective procedure
{}
top
require
n >= 1
ensure
nb
= n
top
=
nb
t
.item(
top
) = 1
empty
(n:
INTEGER_32
)
effective procedure
{}
top
require
n >= 1
ensure
nb
= n
top
= 1
nb
:
INTEGER_32
effective function
{
HANOI
}
top
show_a_discus
(d:
INTEGER_32
, picture:
STRING
)
effective procedure
{
HANOI
}
top
require
1 <= d
d <=
nb
picture /= Void
remove_discus
:
INTEGER_32
effective function
{
HANOI
}
top
ensure
top
>= 1
add_discus
(d:
INTEGER_32
)
effective procedure
{
HANOI
}
top
ensure
top
<=
nb