indexing
	description: "Temporal intervals"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

deferred class interface
	DURATION

feature -- Access

	zero: like Current
			-- Neutral element for "+" and "-"
			-- (from GROUP_ELEMENT)
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
	
feature -- Comparison

	infix "<" (other: like Current): BOOLEAN
			-- Is current object less than other?
			-- (from PART_COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void

	infix "<=" (other: like Current): BOOLEAN
			-- Is current object less than or equal to other?
			-- (from PART_COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void

	infix ">" (other: like Current): BOOLEAN
			-- Is current object greater than other?
			-- (from PART_COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void

	infix ">=" (other: like Current): BOOLEAN
			-- Is current object greater than or equal to other?
			-- (from PART_COMPARABLE)
		require -- from PART_COMPARABLE
			other_exists: other /= void
	
feature -- Status report

	is_negative: BOOLEAN
			-- Is duration negative?

	is_positive: BOOLEAN
			-- Is duration positive?

	is_zero: BOOLEAN
			-- Is duration zero?
	
feature -- Element change

	prefix "+": like Current
			-- Unary plus
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			result_definition: Result.is_equal (Current)

	infix "-" (other: like Current): like Current
			-- Difference with other
		require -- from GROUP_ELEMENT
			other_exists: other /= void
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
	
feature -- Basic operations

	infix "+" (other: like Current): like Current
			-- Sum with other (commutative)
			-- (from GROUP_ELEMENT)
		require -- from GROUP_ELEMENT
			other_exists: other /= void
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			commutative: Result.is_equal (other + Current)

	prefix "-": like Current
			-- Unary minus
			-- (from GROUP_ELEMENT)
		ensure -- from GROUP_ELEMENT
			result_exists: Result /= void
			result_definition: (Result + Current).is_equal (zero)
	
invariant

	sign_correctness: is_positive xor is_negative xor is_zero
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from GROUP_ELEMENT
	neutral_addition: Current.is_equal (Current + zero)
	self_subtraction: zero.is_equal (Current - Current)

end -- class DURATION