GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
tutorial
>
DATE
+
Point of view
All features
ANY
DATE
All features
class DATE
Summary
top
Special
DATE
class to fit with the
PARKING
example.
Direct parents
Insert list:
ANY
Class invariant
top
day
>= 0
min
.in_range(0, 24 * 60 - 1)
Overview
top
Creation features
{
ANY
}
make
(vday:
INTEGER_32
, vmin:
INTEGER_32
)
Features
{
ANY
}
display_on
(stream:
OUTPUT_STREAM
)
To display
Current
on
stream
.
minutes_to
(after: DATE):
INTEGER_32
Count of minutes to go to
after
.
day_night_to
(d2: DATE):
TUPLE 2
[
INTEGER_32
,
INTEGER_32
]
The
Result
is a couple of INTEGER where:
Result.first: Night time.
infix ">="
(d2: DATE):
BOOLEAN
day_time
:
BOOLEAN
Is it Sunny ?
nigth_time
:
BOOLEAN
Is it the night ?
Modifications:
{
ANY
}
make
(vday:
INTEGER_32
, vmin:
INTEGER_32
)
add_time
(nb_min:
INTEGER_32
)
{
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
}
top
To display
Current
on
stream
.
minutes_to
(after: DATE):
INTEGER_32
effective function
{
ANY
}
top
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
}
top
The
Result
is a couple of INTEGER where:
Result.first: Night time.
Result.second: Day time.
require
d2
>=
Current
ensure
Result.first + Result.second =
minutes_to
(d2)
infix ">="
(d2: DATE):
BOOLEAN
effective function
{
ANY
}
top
require
d2 /= Void
day_time
:
BOOLEAN
effective function
{
ANY
}
top
Is it Sunny ?
nigth_time
:
BOOLEAN
effective function
{
ANY
}
top
Is it the night ?
make
(vday:
INTEGER_32
, vmin:
INTEGER_32
)
effective procedure
{
ANY
}
top
ensure
day
= vday
min
= vmin
add_time
(nb_min:
INTEGER_32
)
effective procedure
{
ANY
}
top
day
:
INTEGER_32
writable attribute
{
DATE
}
top
(No
hour
attribute because the number of hours is in
min
value.)
min
:
INTEGER_32
writable attribute
{
DATE
}
top
(No
hour
attribute because the number of hours is in
min
value.)