+
Point of view
All features
class DATE
Summary
Special DATE class to fit with the PARKING example.
Direct parents
Insert list: ANY
Class invariant
Overview
Creation features
{ANY}
Features
{ANY}
Modifications:
{ANY}
{DATE}
  • day: INTEGER_32
    (No hour attribute because the number of hours is in min value.)
  • min: INTEGER_32
    (No hour attribute because the number of hours is in min value.)
display_on (stream: OUTPUT_STREAM)
effective procedure
{ANY}
To display Current on stream.
minutes_to (after: DATE): INTEGER_32
effective function
{ANY}
Count of minutes to go to after.
require
  • after >= Current
ensure
  • Result >= 0
day_night_to (d2: DATE): TUPLE 2[INTEGER_32, INTEGER_32]
effective function
{ANY}
The Result is a couple of INTEGER where:
   Result.first: Night time.
   Result.second: Day time.
require
  • d2 >= Current
ensure
infix ">=" (d2: DATE): BOOLEAN
effective function
{ANY}
require
  • d2 /= Void
day_time: BOOLEAN
effective function
{ANY}
Is it Sunny ?
nigth_time: BOOLEAN
effective function
{ANY}
Is it the night ?
make (vday: INTEGER_32, vmin: INTEGER_32)
effective procedure
{ANY}
ensure
add_time (nb_min: INTEGER_32)
effective procedure
{ANY}
writable attribute
(No hour attribute because the number of hours is in min value.)
writable attribute
(No hour attribute because the number of hours is in min value.)