Home Page ] [ Eiffel Archive ] [ Eiffel Classes and Clusters ]

Arc de Triomphe clipart (2486 bytes)Cardiff Date/Time Cluster


Written by Christine Hollinshead

cardiff.zip (11,187 bytes)


Also available modified by Peter Webb

date_time.tar.gz (8704 bytes)


Licence

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.

Overview

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 ]