/**
 * The refinement mapping for the SortedSet specification.
 * 
 * Project <A HREF = "http://gloss.di.fc.ul.pt/quest/"> Quest</A>.
 * 
 * @author Gloss
 * @version 1.0 - 23/Nov/2012
 **/
 
refinement <E>  

  TotalOrder is E { 
    geq: Orderable e:Orderable is boolean isGreaterEq(E e);
  }
  
  SortedSet[TotalOrder] is TreeSet<E> {
    empty: --> SortedSet[Orderable] is            
    				TreeSet();
    insert: SortedSet[Orderable] e:Orderable --> SortedSet[Orderable] is 
            		void add(E e);
    isEmpty: SortedSet[Orderable] is 
    				boolean isEmpty();
    isIn: SortedSet[Orderable] e:Orderable is 
    				boolean isIn(E e);
    isSubset: SortedSet[Orderable] s:SortedSet[Orderable] is 
    				boolean isSubset(TreeSet<E> s);
    largest: SortedSet[Orderable] -->? Orderable is E last();
    union: SortedSet[Orderable] s:SortedSet[Orderable] --> SortedSet[Orderable] is 
    			void addAll(TreeSet<E> s);
    tailSet: SortedSet[Orderable] e:Orderable --> SortedSet[Orderable] is TreeSet<E> tailSet(E e);
    
  }
  
end refinement