Cardiff Date/Time Cluster[ Home Page ] [ Eiffel Archive ] [ Eiffel Classes and Clusters ]
Cardiff Date/Time ClusterWritten by Christine Hollinshead
cardiff.zip (11,187 bytes)
Also available modified by Peter Webb
date_time.tar.gz (8704 bytes)
Copyright © 1994 University of Wales College of Cardiff
UWCC COMMA PO Box 916 Cardiff CF2 4YN, Wales UK, +44 -222 874812
All rights reserved.
Permission is granted to anyone to make or distribute copies of this software provided that the copyright notice and this permission notice are preserved. Ownership remains with University of Wales College of Cardiff.
This cluster is designed to support the creation and manipulation of dates and times within the Gregorian calendar system.
DATE represents dates within the Gregorian calendar (year, month, day).
DATE_AND_WEEK extends DATE to incorporate information about which day of the week is involved (this class is not in the current distribution).
DATE_AND_TIME extends DATE by the inclusion of time information (hour, minute, second).
GREGORIAN_FUNCTIONS contains the values of constants used by the above classes. All the features in this class are private.
SYSTEM_CLOCK reads the date and time from the system clock into an area of memory. The individual values for year, month, day, hour, minute and second can then be accessed. This class is compatible with SPARC SunOS 4.1.3. Other systems may require that this class is rewritten. In the case of a rewrite the following features are required: read, year, month, day, hour, minute, second (see short/flat form of the class, below).
Short/Flat forms of the classes follow.
class interface DATE
creation
make, make_to_now, make_to_day_of_year
feature specification {ANY}
day,
month,
year : INTEGER
make (yyear, mmonth, dday : INTEGER)
-- Set `day', `month' and `year'.
-- A zero argument sets the corresponding feature to the
value supplied
-- by the system clock.
require
year_valid : yyear >= 0;
month_valid : (mmonth >= 0) and (mmonth <=
12);
day_valid : (dday >= 0) and (dday <= 31);
make_to_now
-- Set to current date, as supplied by the system clock.
make_to_day_of_year (yyear, doy : INTEGER)
-- Set `month' and `day' by its ordinal day number in the
year.
-- A zero argument sets the corresponding feature to the
value supplied
-- by the system clock.
require
year_valid : yyear >= 0;
doy_valid : (0 <= doy) and (doy <= dily);
was_set : BOOLEAN
-- Did the make operation chosen to create the object result
in
-- a valid date being set?
day_of_year : INTEGER
-- Ordinal number of the day in the year in the `Current'
-- instance (1st January = 1).
require
current_set : was_set;
is_leap_year : BOOLEAN
-- Is `year' a leap year?
require
year_valid : was_set;
add_days (ds : INTEGER)
-- Advances `Current' by `ds' days.
require
current_set : was_set;
ensure
Current.days_between (old clone (Current)) = ds;
days_between (other : like
Current) : INTEGER
-- Days between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
infix "<" (other : like
Current) : BOOLEAN
-- Is `Current' date less than `other'?
require
other_not_void : other /= void;
ensure
other_not_less_or_equal : Result = (not (other
<= Current));
consistent : Result implies (not
(other <= Current));
not_reflexive : (Current = other) implies (not
Result);
is_equal (other : like
Current) : BOOLEAN
require
other_not_void : other /= void;
hash_code : INTEGER
ensure
non_negative : Result >= 0;
add_years (ys : INTEGER)
-- Advances `Current' by `ys' years. If a leap year has
a number
-- of whole years added to 29th February then `day' will be
-- reset to 28, unless the resultant year is also a leap
year.
require
current_set : was_set;
years_between (other : like
Current) : INTEGER
-- Whole years between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
add_months (ms : INTEGER)
-- Advances `Current' by `ms' months. Whole months are
added,
-- with `day' being rounded down if `new month' is shorter
than
-- `old month'.
require
current_set : was_set;
months_between (other : like
Current) : INTEGER
-- Whole months between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
feature specification
-- Features from PART_COMPARABLE
infix "<=" (other : like
Current) : BOOLEAN
-- Is `Current' less than or equal to `other'?
--
-- Effects the deferred feature from PART_COMPARABLE.
require
other_not_void : other /= void;
ensure
other_not_less : Result = (not (other <
Current));
consistent : Result implies (not
(other < Current));
reflexive : (Current = other) implies Result;
feature specification
-- Other useful features for comparable
objects.
compare (other : like
Current) : INTEGER
-- Compare `Current' with `other':
-- `< 0' if `Current < other';
-- `0' if `Current = other';
-- `> 0' if `Current > other'.
require
other_not_void : other /= void;
ensure
negative_condition : (Result < 0) = (Current < other);
zero_condition : (Result = 0) = (not ((Current
< other) or (Current > other)));
positive_condition : (Result > 0) = (Current > other);
min (other : like Current) : like
Current
-- The smaller of `Current' and `other'.
require
other_not_void : other /= void;
ensure
less_or_equal_both : (Result <= Current) and then
(Result <= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
max (other : like Current) : like
Current
-- The larger of `Current' and `other'.
require
other_not_void : other /= void;
ensure
greater_or_equal_both : (Result >= Current) and then
(Result >= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
feature specification
-- Effective routines whose behavior are
implied by the behavior of
-- `infix "<"' and `infix
"<="'.
infix ">" (other : like
Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void : other /= void;
ensure
other_is_less : Result = (other < Current);
infix ">=" (other : like
Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void : other /= void;
ensure
other_less_or_equal : Result = (other <= Current);
feature specification {ANY}
dily : INTEGER is 366
-- Days in leap year
invariant
0 < year;
0 <= month;
month <= 12;
0 <= day;
was_set implies (day <=
month_in_days (month, year));
end interface -- class DATE
-- Dates following the Gregorian calendar, with time
class interface DATE_AND_TIME
creation
make, make_to_now, make_to_day_of_year
feature specification {ANY}
hour,
minute,
second : INTEGER
make_to_day_of_year (yyear, doy, hhour,
mminute, ssecond : INTEGER)
-- Set `month' and `day' by its ordinal day number in the
year.
-- A zero value for 'yyear` and/or `doy' sets the corresponding
features
-- to the values supplied by the system clock.
require
year_valid : yyear >= 0;
doy_valid : (0 <= doy) and (doy <= 366);
hour_valid : (0 <= hhour) and (hhour <
24);
minute_valid : (0 <= mminute) and (mminute
< 60);
second_valid : (0 <= ssecond) and (ssecond
< 60);
make (yyear, mmonth, dday, hhour, mminute,
ssecond : INTEGER)
-- Set `day', `month', `year', `hour', `minute' and `second'.
-- A zero argument for `day', `month' and/or `year' sets the
-- corresponding feature to the value supplied by the system
clock.
require
year_valid : yyear >= 0;
month_valid : (0 <= mmonth) and (mmonth <=
12);
day_valid : (0 <= dday) and (dday <= 31);
hour_valid : (0 <= hhour) and (hhour <
24);
minute_valid : (0 <= mminute) and (mminute
< 60);
second_valid : (0 <= ssecond) and (ssecond
< 60);
make_to_now
-- Set to current date and time, as supplied by the system
clock
infix "<" (other : like
Current) : BOOLEAN
-- Is `Current' date less than `other'?
require
other_not_void : other /= void;
ensure
other_not_less_or_equal : Result = (not (other
<= Current));
consistent : Result implies (not
(other <= Current));
not_reflexive : (Current = other) implies (not
Result);
seconds_between (other : like
Current) : INTEGER
-- Seconds between two dates with times
is_equal (other : like
Current) : BOOLEAN
hash_code : INTEGER
ensure
non_negative : Result >= 0;
add_hours (hrs : INTEGER)
-- Advance `Current' by `hrs' hours
ensure
Current.hours_between (old clone (Current)) =
hrs;
hours_between (other : like
Current) : INTEGER
-- Hours between two dates with times
require
other_exists : other /= void;
other_set : other.was_set;
add_minutes (mins : INTEGER)
-- Advance `Current' by `mins' minutes
ensure
Current.minutes_between (old clone (Current)) =
mins;
minutes_between (other : like
Current) : INTEGER
-- Minutes between two dates with times
require
other_exists : other /= void;
other_set : other.was_set;
add_seconds (secs : INTEGER)
-- Advance `Current' by `secs' seconds
ensure
Current.seconds_between (old clone (Current)) =
secs;
feature specification {ANY}
day,
month,
year : INTEGER
make_date (yyear, mmonth, dday : INTEGER)
-- Set `day', `month' and `year'.
-- A zero argument sets the corresponding feature to the value
supplied
-- by the system clock.
require
year_valid : yyear >= 0;
month_valid : (mmonth >= 0) and (mmonth <=
12);
day_valid : (dday >= 0) and (dday <= 31);
date_make_to_day_of_year (yyear, doy :
INTEGER)
-- Set `month' and `day' by its ordinal day number in the year.
-- A zero argument sets the corresponding feature to the value
supplied
-- by the system clock.
require
year_valid : yyear >= 0;
doy_valid : (0 <= doy) and (doy <= dily);
was_set : BOOLEAN
-- Did the make operation chosen to create the object result in
-- a valid date being set?
day_of_year : INTEGER
-- Ordinal number of the day in the year in the `Current'
-- instance (1st January = 1).
require
current_set : was_set;
is_leap_year : BOOLEAN
-- Is `year' a leap year?
require
year_valid : was_set;
add_days (ds : INTEGER)
-- Advances `Current' by `ds' days.
require
current_set : was_set;
ensure
Current.days_between (old clone (Current)) = ds;
days_between (other : like
Current) : INTEGER
-- Days between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
date_is_equal (other : like
Current) : BOOLEAN
require
other_not_void : other /= void;
add_years (ys : INTEGER)
-- Advances `Current' by `ys' years. If a leap year has a
number
-- of whole years added to 29th February then `day' will be
-- reset to 28, unless the resultant year is also a leap year.
require
current_set : was_set;
years_between (other : like
Current) : INTEGER
-- Whole years between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
add_months (ms : INTEGER)
-- Advances `Current' by `ms' months. Whole months are
added,
-- with `day' being rounded down if `new month' is shorter than
-- `old month'.
require
current_set : was_set;
months_between (other : like
Current) : INTEGER
-- Whole months between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
feature specification
-- Features from
PART_COMPARABLE
infix "<=" (other : like
Current) : BOOLEAN
-- Is `Current' less than or equal to `other'?
--
-- Effects the deferred feature from PART_COMPARABLE.
require
other_not_void : other /= void;
ensure
other_not_less : Result = (not (other <
Current));
consistent : Result implies (not
(other < Current));
reflexive : (Current = other) implies Result;
feature specification
-- Other useful features for comparable
objects.
compare (other : like
Current) : INTEGER
-- Compare `Current' with `other':
-- `< 0' if `Current < other';
-- `0' if `Current = other';
-- `> 0' if `Current > other'.
require
other_not_void : other /= void;
ensure
negative_condition : (Result < 0) = (Current < other);
zero_condition : (Result = 0) = (not ((Current
< other) or (Current > other)));
positive_condition : (Result > 0) = (Current > other);
min (other : like Current) : like
Current
-- The smaller of `Current' and `other'.
require
other_not_void : other /= void;
ensure
less_or_equal_both : (Result <= Current) and then
(Result <= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
max (other : like Current) : like
Current
-- The larger of `Current' and `other'.
require
other_not_void : other /= void;
ensure
greater_or_equal_both : (Result >= Current) and then
(Result >= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
feature specification
-- Effective routines whose behavior are
implied by the behavior of
-- `infix "<"' and `infix
"<="'.
infix ">" (other : like
Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void : other /= void;
ensure
other_is_less : Result = (other < Current);
infix ">=" (other : like
Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void : other /= void;
ensure
other_less_or_equal : Result = (other <= Current);
feature specification {ANY}
dily : INTEGER is 366
-- Days in leap year
invariant
0 <= hour;
hour < 24;
0 <= minute;
minute < 60;
0 <= second;
second < 60;
0 < year;
0 <= month;
month <= 12;
0 <= day;
was_set implies (day <=
month_in_days (month, year));
end interface -- class DATE_AND_TIME
-- Gregorian calendar dates with day-of-week features
class interface DATE_AND_WEEK
creation
make_date, make, make_to_now,
make_to_day_of_year
feature specification
day_of_week : INTEGER
-- Day of the week. 0 = Sunday.
-- Found using Zeller's formula.
-- Produces incorrect results for dates before 14 Sept 1752.
require
valid : (year > 1752) or ((year = 1752) and
((month > 9) or ((month = 9) and
(day >= 14))));
make (yyear, mmonth, n, dow : INTEGER)
-- Set date to the n'th dow in a given month and year
-- e.g. the 3nd Tuesday in January, 1994 would be (1994, 01, 3,
2)
-- given that Sunday = 0, Monday = 1 ....
-- Zero values of yyear and mmonth will cause these to be set to
the
-- current values.
require
month_valid : (0 < mmonth) and (mmonth <=
12);
year_valid : ((yyear = 0) or (yyear > 1752)) or
((yyear = 1752) and (month > 9));
n_valid : (0 < n) and (n <= 5);
dow_valid : (0 <= dow) and (dow < 7);
feature specification {ANY}
day,
month,
year : INTEGER
make_date (yyear, mmonth, dday : INTEGER)
-- Set `day', `month' and `year'.
-- A zero argument sets the corresponding feature to the value
supplied
-- by the system clock.
require
year_valid : yyear >= 0;
month_valid : (mmonth >= 0) and (mmonth <=
12);
day_valid : (dday >= 0) and (dday <= 31);
make_to_now
-- Set to current date, as supplied by the system clock.
make_to_day_of_year (yyear, doy : INTEGER)
-- Set `month' and `day' by its ordinal day number in the year.
-- A zero argument sets the corresponding feature to the value
supplied
-- by the system clock.
require
year_valid : yyear >= 0;
doy_valid : (0 <= doy) and (doy <= dily);
was_set : BOOLEAN
-- Did the make operation chosen to create the object result in
-- a valid date being set?
day_of_year : INTEGER
-- Ordinal number of the day in the year in the `Current'
-- instance (1st January = 1).
require
current_set : was_set;
is_leap_year : BOOLEAN
-- Is `year' a leap year?
require
year_valid : was_set;
add_days (ds : INTEGER)
-- Advances `Current' by `ds' days.
require
current_set : was_set;
ensure
Current.days_between (old clone (Current)) = ds;
days_between (other : like
Current) : INTEGER
-- Days between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
infix "<" (other : like
Current) : BOOLEAN
-- Is `Current' date less than `other'?
require
other_not_void : other /= void;
ensure
other_not_less_or_equal : Result = (not (other
<= Current));
consistent : Result implies (not
(other <= Current));
not_reflexive : (Current = other) implies (not
Result);
is_equal (other : like
Current) : BOOLEAN
require
other_not_void : other /= void;
hash_code : INTEGER
ensure
non_negative : Result >= 0;
add_years (ys : INTEGER)
-- Advances `Current' by `ys' years. If a leap year has a
number
-- of whole years added to 29th February then `day' will be
-- reset to 28, unless the resultant year is also a leap year.
require
current_set : was_set;
years_between (other : like
Current) : INTEGER
-- Whole years between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
add_months (ms : INTEGER)
-- Advances `Current' by `ms' months. Whole months are
added,
-- with `day' being rounded down if `new month' is shorter than
-- `old month'.
require
current_set : was_set;
months_between (other : like
Current) : INTEGER
-- Whole months between two dates.
require
current_set : was_set;
other_exists : other /= void;
other_set : other.was_set;
feature specification
-- Features from
PART_COMPARABLE
infix "<=" (other : like
Current) : BOOLEAN
-- Is `Current' less than or equal to `other'?
--
-- Effects the deferred feature from PART_COMPARABLE.
require
other_not_void : other /= void;
ensure
other_not_less : Result = (not (other <
Current));
consistent : Result implies (not
(other < Current));
reflexive : (Current = other) implies Result;
feature specification
-- Other useful features for comparable
objects.
compare (other : like
Current) : INTEGER
-- Compare `Current' with `other':
-- `< 0' if `Current < other';
-- `0' if `Current = other';
-- `> 0' if `Current > other'.
require
other_not_void : other /= void;
ensure
negative_condition : (Result < 0) = (Current < other);
zero_condition : (Result = 0) = (not ((Current
< other) or (Current > other)));
positive_condition : (Result > 0) = (Current > other);
min (other : like Current) : like
Current
-- The smaller of `Current' and `other'.
require
other_not_void : other /= void;
ensure
less_or_equal_both : (Result <= Current) and then
(Result <= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
max (other : like Current) : like
Current
-- The larger of `Current' and `other'.
require
other_not_void : other /= void;
ensure
greater_or_equal_both : (Result >= Current) and then
(Result >= other);
one_or_the_other : (compare (Result) = 0) or else
(other.compare (Result) = 0);
feature specification
-- Effective routines whose behavior are
implied by the behavior of
-- `infix "<"' and `infix
"<="'.
infix ">" (other : like
Current) : BOOLEAN
-- Is `Current' strictly greater than `other'?
require
other_not_void : other /= void;
ensure
other_is_less : Result = (other < Current);
infix ">=" (other : like
Current) : BOOLEAN
-- Is `Current' greater than or equal to `other'?
require
other_not_void : other /= void;
ensure
other_less_or_equal : Result = (other <= Current);
feature specification {ANY}
dily : INTEGER is 366
-- Days in leap year
invariant
0 < year;
0 <= month;
month <= 12;
0 <= day;
was_set implies (day <=
month_in_days (month, year));
end interface -- class DATE_AND_WEEK
-- Gregorian calendar constants, converters, etc.
class interface GREGORIAN_FUNCTIONS
end interface -- class GREGORIAN_FUNCTIONS
-- Class to access the system clock on a UNIX machine.
class interface SYSTEM_CLOCK
feature specification {ANY}
year : INTEGER
month : INTEGER
day : INTEGER
hour : INTEGER
minute : INTEGER
second : INTEGER
read
-- Reads system clock and stores year, month, day, hour, minute
and
-- second in memory.
end interface -- class SYSTEM_CLOCK
[ Home Page ] [ Eiffel Archive ] [ Eiffel Classes and Clusters ]