GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
tutorial
>
LEVEL
+
Point of view
All features
ANY
All features
class LEVEL
Summary
top
Direct parents
Insert list:
ANY
Class invariant
top
occupied_slot_count
.in_range(0,
capacity
)
free_slot_count
.in_range(0,
capacity
)
occupied_slot_count
+
free_slot_count
=
capacity
Overview
top
Creation features
{
ANY
}
make
(max_cars:
INTEGER_32
)
Features
{
ANY
}
occupied_slot_count
:
INTEGER_32
Total count of occupied places in the
Current
level.
free_slot_count
:
INTEGER_32
Total count of free places in the
Current
level.
capacity
:
INTEGER_32
Of the level.
is_full
:
BOOLEAN
Is this level full?
Modifications:
{
ANY
}
make
(max_cars:
INTEGER_32
)
arrival
(car:
CAR
)
departure
(car_number:
INTEGER_32
, departure_time:
DATE
, hour_price:
REAL_64
):
REAL_64
Gives price to pay or -1 when car is not at this level.
{}
car_slots
:
ARRAY
[
CAR
]
Memory of occupied slots of this level.
occupied_slot_count
:
INTEGER_32
writable attribute
{
ANY
}
top
Total count of occupied places in the
Current
level.
free_slot_count
:
INTEGER_32
effective function
{
ANY
}
top
Total count of free places in the
Current
level.
capacity
:
INTEGER_32
effective function
{
ANY
}
top
Of the level.
is_full
:
BOOLEAN
effective function
{
ANY
}
top
Is this level full?
make
(max_cars:
INTEGER_32
)
effective procedure
{
ANY
}
top
require
max_cars > 0
ensure
occupied_slot_count
= 0
arrival
(car:
CAR
)
effective procedure
{
ANY
}
top
require
car /= Void
not
is_full
ensure
occupied_slot_count
>= old
occupied_slot_count
+ 1
departure
(car_number:
INTEGER_32
, departure_time:
DATE
, hour_price:
REAL_64
):
REAL_64
effective function
{
ANY
}
top
Gives price to pay or -1 when car is not at this level.
require
car_number > 0
car_slots
:
ARRAY
[
CAR
]
writable attribute
{}
top
Memory of occupied slots of this level.