| 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 /= Voidduration (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
|
Copyright © 2000-2001, Eric
Bezault mailto:ericb@gobosoft.com http://www.gobosoft.com Last Updated: 7 April 2001 |