+
Point of view
All features
class PARKING
Summary
Direct parents
Insert list: ANY
Class invariant
Overview
Creation features
{ANY}
Features
{ANY}
Modifications:
{ANY}
{}
lower_level: INTEGER_32
effective function
{ANY}
The actual lowest level number.
upper_level: INTEGER_32
effective function
{ANY}
The actual upper most level number.
hour_price: REAL_64
writable attribute
{ANY}
The day time price to pay per hour.
clock: DATE
writable attribute
{ANY}
The parking clock.
occupied_slot_count: INTEGER_32
effective function
{ANY}
Total number of cars inside the parking.
level_occupied_slot_count (level_number: INTEGER_32): INTEGER_32
effective function
{ANY}
Total number of cars in the given level_number.
require ensure
  • Result >= 0
arrival: INTEGER_32
effective function
{ANY}
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}
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}
set_hour_price (hp: REAL_64)
effective procedure
{ANY}
require
  • hp >= 0
ensure
default_hour_price: REAL_64
is 1.50
constant attribute
{}
make (ll: ARRAY[LEVEL])
effective procedure
{}
require
  • ll /= Void
ensure
level_list: ARRAY[LEVEL]
writable attribute
{}
last_car_number: INTEGER_32
writable attribute
{}
Used to give different numbers for cars.