indexing
description: "Absolute temporal values"
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
access: date, time
deferred class interface
ABSOLUTE
feature
origin: like Current
ensure
result_exists: Result /= void
feature
duration: DURATION
origin
feature
is_equal (other: like Current): BOOLEAN
other
COMPARABLE
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
max (other: like Current): like Current
other
COMPARABLE
require COMPARABLE
other_exists: other /= void
ensure COMPARABLE
current_if_not_smaller: Current >= other implies Result = Current
other_if_smaller: Current < other implies Result = other
min (other: like Current): like Current
other
COMPARABLE
require COMPARABLE
other_exists: other /= void
ensure COMPARABLE
current_if_not_greater: Current <= other implies Result = Current
other_if_greater: Current > other implies Result = other
three_way_comparison (other: like Current): INTEGER
other
COMPARABLE
require COMPARABLE
other_exists: other /= void
ensure COMPARABLE
equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = - 1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)
infix "<" (other: like Current): BOOLEAN
other
require PART_COMPARABLE
other_exists: other /= void
ensure then COMPARABLE
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
other
COMPARABLE
require PART_COMPARABLE
other_exists: other /= void
ensure then COMPARABLE
definition: Result = ((Current < other) or is_equal (other))
infix ">" (other: like Current): BOOLEAN
other
COMPARABLE
require PART_COMPARABLE
other_exists: other /= void
ensure then COMPARABLE
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
other
COMPARABLE
require PART_COMPARABLE
other_exists: other /= void
ensure then COMPARABLE
definition: Result = (other <= Current)
feature
relative_duration (other: like Current): DURATION
Currentother
require
other_exists: other /= void
ensure
result_exists: Result /= void
infix "-" (other: like Current): INTERVAL [like Current]
other
require
other_exists: other /= void
other_smaller_than_current: other <= Current
ensure
result_exists: Result /= void
result_set: Result.start_bound.is_equal (other) and then Result.end_bound.is_equal (Current)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
COMPARABLE
irreflexive_comparison: not (Current < Current)
end -- ABSOLUTE