deferred class interface COMPARABLE
   -- 
   --  All class handling COMPARABLE object with a total order relation
   --  should inherit from this class.
   -- 

feature(s) from COMPARABLE
   infix "<" (other: like Current): BOOLEAN
      --  Is Current strictly less than other?
      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other < Current)

   infix "<=" (other: like Current): BOOLEAN
      --  Is Current less or equal other?
      require
         other_exists: other /= Void
      ensure
         definition: Result = (Current < other or is_equal(other))

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

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

   in_range (lower, upper: like Current): BOOLEAN
      --  Return true if Current is in range [lower..upper]
      ensure
         Result = (Current >= lower and Current <= upper)

   compare (other: like Current): INTEGER
      --  Compare Current with other.
      --  <  <==> Result < 0
      --  >  <==> Result > 0
      --  Otherwise Result = 0.
      require
         other /= Void
      ensure
         Result < 0 = Current < other;
         Result = 0 = not (Current < other or Current > other);
         Result > 0 = Current > other

   min (other: like Current): like Current
      --  Minimum of Current and other.
      require
         other /= Void
      ensure
         Result <= Current and then Result <= other;
         compare(Result) = 0 or else other.compare(Result) = 0

   max (other: like Current): like Current
      --  Maximum of Current and other.
      require
         other /= Void
      ensure
         Result >= Current and then Result >= other;
         compare(Result) = 0 or else other.compare(Result) = 0


end of deferred COMPARABLE