Class DT_ABSOLUTE_TIME |

    note

>     description:

>         "Absolute temporal notion"

>     library:    "Gobo Eiffel Time Library"
>     copyright:  "Copyright (c) 2000-2001, Eric Bezault and others"
>     license:    "MIT License"

    deferred class interface

>     DT_ABSOLUTE_TIME

    inherit

>     COMPARABLE
>     HASHABLE

    feature -- Access

>     infix "-" (other: like Current): like duration
>             -- Duration between other and Current
>         require
>             other_not_void: other /= Void
>         ensure
>             duration_not_void: Result /= Void
>             definition: (other + Result).is_equal (Current)

>     infix "+" (a_duration: like 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

>     duration (other: like Current): DT_DURATION
>             -- Duration between other and Current
>         require
>             other_not_void: other /= Void
>         deferred
>         ensure
>             duration_not_void: Result /= Void
>             definition: (other + Result).is_equal (Current)

>     hash_code: INTEGER
>             -- Hash code value
>             -- (From HASHABLE.)
>         deferred
>         ensure
>             good_hash_value: Result >= 0

    feature -- Comparison

>     infix "<" (other: like Current): BOOLEAN
>             -- Is current object less than other?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         deferred
>         ensure
>             asymmetric: Result implies not (other < Current)

>     infix "<=" (other: like Current): BOOLEAN
>             -- Is current object less than or equal to other?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         ensure
>             definition: Result = ((Current < other) or is_equal (other))

>     infix ">=" (other: like Current): BOOLEAN
>             -- Is current object greater than or equal to other?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         ensure
>             definition: Result = (other <= Current)

>     infix ">" (other: like Current): BOOLEAN
>             -- Is current object greater than other?
>             -- (From COMPARABLE.)
>         require
>             other_exists: other /= Void
>         ensure
>             definition: Result = (other < Current)

>     is_equal (other: like Current): BOOLEAN
>             -- Is other attached to an object considered equal
>             -- to current object?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         ensure
>             symmetric: Result implies other.is_equal (Current)
>             consistent: standard_is_equal (other) implies Result
>             trichotomy: Result = (not (Current < other) and not (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)

    feature -- Duplication

>     copy (other: like Current)
>             -- Copy other to current time.
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>             type_identity: same_type (other)
>         ensure
>             is_equal: is_equal (other)

    feature -- Element change

>     add_duration (a_duration: like duration)
>             -- Add a_duration to Current.
>         require
>             a_duration_not_void: a_duration /= Void
>         deferred

    invariant

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

    end -- class DT_ABSOLUTE_TIME