Class DT_ABSOLUTE

Class DT_ABSOLUTE_TIME

note

description:

    "Absolute temporal notion"

library:    "Gobo Eiffel Time Library"
author:     "Eric Bezault <ericb@gobosoft.com>"
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