elogger API
Overview Classes Cluster Class Index          Top Features

time.date

Class DT_DATE


Direct ancestors

DT_ABSOLUTE_TIME, DT_DATE_VALUE, DT_GREGORIAN_CALENDAR, DT_SHARED_WEEK_DAYS_FROM_MONDAY, DT_DATE_HANDLER

Known direct descendants

DT_DATE_TIME

Creation

Features

Invariants

indexing

description

Dates (Gregorian calendar)

remark

year 0 means 1 BCE, year -1 means 2 BCE, etc.

library

Gobo Eiffel Time Library

copyright

Copyright (c) 2000-2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

class DT_DATE

inherit

DT_ABSOLUTE_TIME
COMPARABLE
HASHABLE
KL_CLONABLE
DT_DATE_VALUE
KL_IMPORTED_STRING_ROUTINES
KL_IMPORTED_INTEGER_ROUTINES
DT_GREGORIAN_CALENDAR
KL_GREGORIAN_CALENDAR
DT_DATE_HANDLER

create

make (y, m, d: INTEGER)

-- Create a new date.

require

m_large_enough: m >= January
m_small_enough: m <= December
d_large_enough: d >= 1
d_small_enough: d <= days_in_month (m, y)

ensure

year_set: year = y
month_set: month = m
day_set: day = d

make_from_day_count (d: INTEGER)

-- Create a new date from the number
-- of days since epoch (1 Jan 1970).

ensure

day_count_set: day_count = d

create {DT_DATE_HANDLER}

make_from_storage (a_storage: INTEGER)

-- Create a new date from a_storage.

ensure

storage_set: storage = a_storage

feature -- Access

infix "+" (a_duration: like duration): like Current

-- Addition of a_duration to Current
-- (Create a new object at each call.)
-- (From DT_ABSOLUTE_TIME)

require

a_duration_not_void: a_duration /= Void

ensure

addition_not_void: Result /= Void

infix "-" (other: like Current): like duration

-- Duration between other and Current
-- (From DT_ABSOLUTE_TIME)

require

other_not_void: other /= Void

ensure

duration_not_void: Result /= Void
definition: (other + Result).is_equal (Current)

week_number (y, m, d: INTEGER): INTEGER

-- Week number for date of year y, month m and day d,
-- using ISO 8601 specification: weeks start on Monday and
-- week number 1 contains the first Thursday of the year.
-- Dates before the first week of the year have the week
-- number of of last day of the previous year.
-- (From DT_GREGORIAN_CALENDAR)

require

m_large_enough: m >= January
m_small_enough: m <= December
d_large_enough: d >= 1
d_small_enough: d <= days_in_month (m, y)

ensure

week_number_large_enough: Result >= 1
week_number_small_enough: Result <= 53

INTEGER_: KL_INTEGER_ROUTINES

-- Routines that ought to be in class INTEGER_32
-- (From KL_IMPORTED_INTEGER_ROUTINES)

ensure

integer_routines_not_void: Result /= Void

canonical_duration (other: like Current): like duration

-- Canonical duration between other and Current

require

other_not_void: other /= Void

ensure

duration_not_void: Result /= Void
canonical_duration: Result.is_canonical (other)
definition: (other + Result).is_equal (Current)

date_duration (other: like Current): DT_DATE_DURATION

-- Duration between other and Current

require

other_not_void: other /= Void

ensure

date_duration_not_void: Result /= Void
definite_duration: Result.is_definite
definition: (other &@ Result).is_equal (Current)

day: INTEGER

-- Day
-- (From DT_DATE_VALUE)

ensure then

day_large_enough: Result >= 1
day_small_enough: Result <= days_in_month (month, year)

day_count: INTEGER

-- Number of days since epoch (1 Jan 1970)

day_of_week: DT_WEEK_DAY

-- Day of week for Current

ensure

day_of_week_not_void: Result /= Void

days_in_current_month: INTEGER

-- Number of days in Current's month

ensure

at_least_one: Result >= 1
max_days_in_month: Result <= Max_days_in_month

days_in_previous_month: INTEGER

-- Number of days in Current's previous month

ensure

at_least_one: Result >= 1
max_days_in_month: Result <= Max_days_in_month

duration (other: like Current): DT_DATE_DURATION

-- Duration between other and Current
-- (From DT_ABSOLUTE_TIME)

require

other_not_void: other /= Void

ensure

duration_not_void: Result /= Void
definition: (other + Result).is_equal (Current)

ensure then

definite_duration: Result.is_definite

hash_code: INTEGER

-- Hash code
-- (From HASHABLE)

ensure

good_hash_value: Result >= 0

infix "&@" (a_duration: like date_duration): like Current

-- Addition of a_duration to Current
-- (Create a new object at each call.)

require

a_duration_not_void: a_duration /= Void

ensure

addition_not_void: Result /= Void

month: INTEGER

-- Month
-- (From DT_DATE_VALUE)

ensure then

month_large_enough: Result >= January
month_small_enough: Result <= December

week: INTEGER

-- Week number for Current using ISO 8601 specification:
-- weeks start on Monday and week number 1 contains the
-- first Thursday of the year. Dates before the first week
-- of the year have the week number of of last day of
-- the previous year.

week_day: INTEGER

-- Day of week for Current

obsolete

[041224] Use day_of_week instead.

ensure

valid_day: Result >= Sunday and Result <= Saturday

year: INTEGER

-- Year
-- (From DT_DATE_VALUE)

year_day: INTEGER

-- Day in current year

ensure

non_leap_year: not is_leap_year implies (Result >= 1 and Result <= Days_in_year)
leap_year: is_leap_year implies (Result >= 1 and Result <= Days_in_leap_year)

STRING_: KL_STRING_ROUTINES

-- Routines that ought to be in class STRING_8
-- (From KL_IMPORTED_STRING_ROUTINES)

ensure

string_routines_not_void: Result /= Void

feature -- Comparison

infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?
-- (From PART_COMPARABLE)

require

other_exists: other /= Void

ensure then

definition: Result = ((Current < other) or is_equal (other))

infix ">" (other: like Current): BOOLEAN

-- Is current object greater than other?
-- (From PART_COMPARABLE)

require

other_exists: other /= Void

ensure then

definition: Result = (other < Current)

infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to other?
-- (From PART_COMPARABLE)

require

other_exists: other /= Void

ensure then

definition: Result = (other <= Current)

max (other: like Current): like Current

-- The greater of current object and other
-- (From COMPARABLE)

require

other_exists: other /= Void

ensure

current_if_not_smaller: Current >= other implies Result = Current
other_if_smaller: Current < other implies Result = other

min (other: like Current): like Current

-- The smaller of current object and other
-- (From COMPARABLE)

require

other_exists: other /= Void

ensure

current_if_not_greater: Current <= other implies Result = Current
other_if_greater: Current > other implies Result = other

three_way_comparison (other: like Current): INTEGER

-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
-- (From COMPARABLE)

require

other_exists: other /= Void

ensure

equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = -1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)

infix "<" (other: like Current): BOOLEAN

-- Is Current before other on the time axis?
-- (From PART_COMPARABLE)

require

other_exists: other /= Void

ensure then

asymmetric: Result implies not (other < Current)

same_date (other: DT_DATE): BOOLEAN

-- Is Current date equal to other?

require

other_not_void: other /= Void

feature -- Status report

is_hashable: BOOLEAN

-- May current object be hashed?
-- (True if it is not its type's default.)
-- (From HASHABLE)

ensure

ok_if_not_default: Result implies (Current /= default)

valid_week (a_week, a_year: INTEGER): BOOLEAN

-- Is a_week a valid ISO 8601 week in a_year?
-- Weeks start on Monday and week number 1 contains
-- the first Thursday of the year.
-- (From DT_GREGORIAN_CALENDAR)

is_leap_year: BOOLEAN

-- Is year a leap year?

feature -- Element change

add_date_duration (a_duration: like date_duration)

-- Add a_duration to Current.
-- (Add a_duration.year and a_duration.month first, then
-- set day to day.min (days_in_month (new_month, new_year))
-- and finally add a_duration.day.)

require

a_duration_not_void: a_duration /= Void

add_days (d: INTEGER)

-- Add d days to Current.

add_duration (a_duration: like duration)

-- Add a_duration to Current.
-- (Add a_duration.year and a_duration.month first, then
-- set day to day.min (days_in_month (new_month, new_year))
-- and finally add a_duration.day.)
-- (From DT_ABSOLUTE_TIME)

require

a_duration_not_void: a_duration /= Void

add_months (m: INTEGER)

-- Add m months to Current.

ensure

day_adjusted: day = (old day).min (days_in_month (month, year))

add_years (y: INTEGER)

-- Add y years to Current.

ensure

day_adjusted: day = (old day).min (days_in_month (month, year))

add_years_months_days (y, m, d: INTEGER)

-- Add y years, m months and d days to Current.
-- (Add y and m first, then set day to
-- day.min (days_in_month (new_month, new_year))
-- and finally add d.)

feature -- Duplication

cloned_object: like Current

-- Clone of current object
-- (From KL_CLONABLE)

ensure

cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)

feature -- Epoch

Epoch_day: INTEGER

-- Epoch date (1 Jan 1970)
-- (From KL_GREGORIAN_CALENDAR)

epoch_days (y, m, d: INTEGER): INTEGER

-- Number of days since epoch date (1 Jan 1970)
-- (From KL_GREGORIAN_CALENDAR)

require

m_large_enough: m >= January
m_small_enough: m <= December
d_large_enough: d >= 1
d_small_enough: d <= days_in_month (m, y)

Epoch_month: INTEGER

Epoch_year: INTEGER

feature -- Month

April: INTEGER

August: INTEGER

days_at_month (m, y: INTEGER): INTEGER

-- Number of days from beginning of year
-- y until beginning of month m
-- (From KL_GREGORIAN_CALENDAR)

require

m_large_enough: m >= January
m_small_enough: m <= December

ensure

days_positive: Result >= 0

days_in_month (m, y: INTEGER): INTEGER

-- Number of days in month m of year y
-- (From KL_GREGORIAN_CALENDAR)

require

m_large_enough: m >= January
m_small_enough: m <= December

ensure

at_least_one: Result >= 1
max_days_in_month: Result <= Max_days_in_month

December: INTEGER

-- Months
-- (From KL_GREGORIAN_CALENDAR)

February: INTEGER

January: INTEGER

July: INTEGER

June: INTEGER

March: INTEGER

Max_days_in_month: INTEGER

-- Maximum number of days in a month
-- (From KL_GREGORIAN_CALENDAR)

May: INTEGER

November: INTEGER

October: INTEGER

September: INTEGER

feature -- Output

append_to_string (a_string: STRING)

-- Append printable representation
-- (year/month/day) to a_string.
-- (From DT_DATE_VALUE)

require

a_string_not_void: a_string /= Void

date_out: STRING

-- Printable representation (year/month/day)
-- (From DT_DATE_VALUE)

ensure

date_out_not_void: Result /= Void

out: STRING

-- Printable representation (year/month/day)
-- (From ANY)

append_date_to_string (a_string: STRING)

-- Append printable representation to a_string.
-- The day and month parts are printing with exactly two digits.
-- (From DT_DATE_VALUE)

require

a_string_not_void: a_string /= Void

feature -- Setting

set_date (a_date: DT_DATE)

-- Set year, month and day from a_date.

require

a_date_not_void: a_date /= Void

ensure

year_set: year = a_date.year
month_set: month = a_date.month
day_set: day = a_date.day

set_day (d: INTEGER)

-- Set day to d.

require

d_large_enough: d >= 1
d_small_enough: d <= days_in_month (month, year)

ensure

day_set: day = d
same_year: year = old year
same_month: month = old month

set_day_count (d: INTEGER)

-- Set day_count to d.

ensure

day_count_set: day_count = d

set_month (m: INTEGER)

-- Set month to m.

require

m_large_enough: m >= January
m_small_enough: m <= December
leap_year_aware: day <= days_in_month (m, year)

ensure

month_set: month = m
same_year: year = old year
same_day: day = old day

set_year (y: INTEGER)

-- Set year to y.

require

leap_year_aware: day <= days_in_month (month, y)

ensure

year_set: year = y
same_month: month = old month
same_day: day = old day

set_year_month_day (y, m, d: INTEGER)

-- Set year to y, month to m and day to d.

require

m_large_enough: m >= January
m_small_enough: m <= December
d_large_enough: d >= 1
d_small_enough: d <= days_in_month (m, y)

ensure

year_set: year = y
month_set: month = m
day_set: day = d

feature -- Time

Hours_in_day: INTEGER

-- Number of hours in a day
-- (From KL_GREGORIAN_CALENDAR)

Milliseconds_in_day: INTEGER

-- Number of milliseconds in a day
-- (From KL_GREGORIAN_CALENDAR)

Minutes_in_hour: INTEGER

-- Number of minutes in an hour
-- (From KL_GREGORIAN_CALENDAR)

Seconds_in_day: INTEGER

-- Number of seconds in a day
-- (From KL_GREGORIAN_CALENDAR)

Seconds_in_hour: INTEGER

-- Number of seconds in an hour
-- (From KL_GREGORIAN_CALENDAR)

Seconds_in_minute: INTEGER

-- Number of seconds in a minute
-- (From KL_GREGORIAN_CALENDAR)

feature -- Week day

Days_in_week: INTEGER

-- Number of days in a week
-- (From KL_GREGORIAN_CALENDAR)

Friday: INTEGER

Monday: INTEGER

next_day (d: INTEGER): INTEGER

-- Week day after d
-- (From KL_GREGORIAN_CALENDAR)

obsolete

[041224] Use next_day from DT_WEEK_DAY instead.

require

d_large_enough: d >= Sunday
d_small_enough: d <= Saturday

ensure

sunday_definition: (d = Sunday) implies (Result = Monday)
monday_definition: (d = Monday) implies (Result = Tuesday)
tuesday_definition: (d = Tuesday) implies (Result = Wednesday)
wednesday_definition: (d = Wednesday) implies (Result = Thursday)
thursday_definition: (d = Thursday) implies (Result = Friday)
friday_definition: (d = Friday) implies (Result = Saturday)
saturday_definition: (d = Saturday) implies (Result = Sunday)

previous_day (d: INTEGER): INTEGER

-- Week day before d
-- (From KL_GREGORIAN_CALENDAR)

obsolete

[041224] Use previous_day from DT_WEEK_DAY instead.

require

d_large_enough: d >= Sunday
d_small_enough: d <= Saturday

ensure

sunday_definition: (d = Sunday) implies (Result = Saturday)
monday_definition: (d = Monday) implies (Result = Sunday)
tuesday_definition: (d = Tuesday) implies (Result = Monday)
wednesday_definition: (d = Wednesday) implies (Result = Tuesday)
thursday_definition: (d = Thursday) implies (Result = Wednesday)
friday_definition: (d = Friday) implies (Result = Thursday)
saturday_definition: (d = Saturday) implies (Result = Friday)

Saturday: INTEGER

-- Week days
-- obsolete
-- "[041224] Use DT_WEEK_DAY instead."
-- (From KL_GREGORIAN_CALENDAR)

Sunday: INTEGER

Thursday: INTEGER

Tuesday: INTEGER

Wednesday: INTEGER

feature -- Year

Days_in_100_years: INTEGER

Days_in_2_leap_years: INTEGER

-- Number of days in multiple years
-- (From KL_GREGORIAN_CALENDAR)

Days_in_2_years: INTEGER

Days_in_3_leap_years: INTEGER

Days_in_3_years: INTEGER

Days_in_400_years: INTEGER

Days_in_4_years: INTEGER

Days_in_leap_year: INTEGER

-- Number of days in a (leap) year
-- (From KL_GREGORIAN_CALENDAR)

Days_in_year: INTEGER

leap_year (y: INTEGER): BOOLEAN

-- Is y a leap year?
-- (From KL_GREGORIAN_CALENDAR)

Months_in_year: INTEGER

-- Number of months in a year
-- ensure
-- definition: Result = (December - Januray + 1)
-- (From KL_GREGORIAN_CALENDAR)

feature {DT_DATE_HANDLER} -- Implementation

set_storage (a_storage: INTEGER)

-- Set storage to a_storage.

ensure

storage_set: storage = a_storage

storage: INTEGER

-- Compact version of Current
-- (INTEGER_32 should have at least 32 bits.)

invariant


-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

-- From COMPARABLE
irreflexive_comparison: not (Current < Current)

Documentation generated by edoc