GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
tutorial
>
PARKING
+
Point of view
All features
ANY
All features
class PARKING
Summary
top
Direct parents
Insert list:
ANY
Class invariant
top
valid_price:
hour_price
>= 0
clock
/= Void
last_car_number
>= 0
level_list
/= Void
Overview
top
Creation features
{
ANY
}
make
(ll:
ARRAY
[
LEVEL
])
Features
{
ANY
}
lower_level
:
INTEGER_32
The actual lowest level number.
upper_level
:
INTEGER_32
The actual upper most level number.
hour_price
:
REAL_64
The day time price to pay per hour.
clock
:
DATE
The parking
clock
.
occupied_slot_count
:
INTEGER_32
Total number of cars inside the parking.
level_occupied_slot_count
(level_number:
INTEGER_32
):
INTEGER_32
Total number of cars in the given
level_number
.
Modifications:
{
ANY
}
arrival
:
INTEGER_32
Arrival of a new car.
departure
(car:
INTEGER_32
):
REAL_64
Gives the price to pay or -1 when cannot be found in the parking.
add_time
(incr:
INTEGER_32
)
set_hour_price
(hp:
REAL_64
)
{}
default_hour_price
:
REAL_64
make
(ll:
ARRAY
[
LEVEL
])
level_list
:
ARRAY
[
LEVEL
]
last_car_number
:
INTEGER_32
Used to give different numbers for cars.
lower_level
:
INTEGER_32
effective function
{
ANY
}
top
The actual lowest level number.
upper_level
:
INTEGER_32
effective function
{
ANY
}
top
The actual upper most level number.
hour_price
:
REAL_64
writable attribute
{
ANY
}
top
The day time price to pay per hour.
clock
:
DATE
writable attribute
{
ANY
}
top
The parking
clock
.
occupied_slot_count
:
INTEGER_32
effective function
{
ANY
}
top
Total number of cars inside the parking.
level_occupied_slot_count
(level_number:
INTEGER_32
):
INTEGER_32
effective function
{
ANY
}
top
Total number of cars in the given
level_number
.
require
level_number.in_range(
lower_level
,
upper_level
)
ensure
Result >= 0
arrival
:
INTEGER_32
effective function
{
ANY
}
top
Arrival of a new car.
The
Result
is the number of the new car or 0 when the parking is full.
ensure
Result >= 0
departure
(car:
INTEGER_32
):
REAL_64
effective function
{
ANY
}
top
Gives the price to pay or -1 when cannot be found in the parking.
require
car > 0
add_time
(incr:
INTEGER_32
)
effective procedure
{
ANY
}
top
set_hour_price
(hp:
REAL_64
)
effective procedure
{
ANY
}
top
require
hp >= 0
ensure
hour_price
= hp
default_hour_price
:
REAL_64
is 1.50
constant attribute
{}
top
make
(ll:
ARRAY
[
LEVEL
])
effective procedure
{}
top
require
ll /= Void
ensure
hour_price
=
default_hour_price
level_list
= ll
last_car_number
= 0
level_list
:
ARRAY
[
LEVEL
]
writable attribute
{}
top
last_car_number
:
INTEGER_32
writable attribute
{}
top
Used to give different numbers for cars.