java.util
Interface SortedSet

All Superinterfaces:

Collection, Set

All Known Implementing Classes:

TreeSet

public interface SortedSet

extends Set

JML's specification of java.util.SortedSet.

Version:

$Revision: 1.9 $

Author:

Katie Becker, Gary T. Leavens

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Set

instance public represents theCollection <- this.theSet.toBag();

Specifications inherited from interface Collection

instance public invariant this.elementType == this.theCollection.elementType; instance public invariant this.containsNull == this.theCollection.containsNull; instance public invariant !this.nullElementsSupported ==> !this.containsNull;

Model Field Summary
[instance]  JMLType	firstElement
[instance]  JMLType	lastElement

 

Model fields inherited from interface java.util.Set

theSet

 

Model fields inherited from interface java.util.Collection

addOperationSupported, elementState, nullElementsSupported, removeOperationSupported, theCollection

 

Ghost Field Summary

 

Ghost fields inherited from interface java.util.Collection

containsNull, elementType

 

Model Method Summary

 

Model methods inherited from interface java.util.Collection

hashValue

 

Method Summary
Comparator	comparator()
Object	first()
SortedSet	headSet(Object toElement)
Object	last()
SortedSet	subSet(Object fromElement, Object toElement)
SortedSet	tailSet(Object fromElement)

 

Methods inherited from interface java.util.Set

add, addAll, clear, contains, containsAll, equals, hashCode, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray

 

Model Field Detail

firstElement

public JMLType firstElement

Specifications: instance

lastElement

public JMLType lastElement

Specifications: instance

comparator

public Comparator comparator()

Specifications: pure

public normal_behavior
ensures true;

subSet

public SortedSet subSet(Object fromElement,
                        Object toElement)

Specifications: (class)pure

public behavior
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(fromElement) or \typeof(toElement) is incompatible with this set's comparator *);
signals (java.lang.IllegalArgumentException) (* fromElement > toElement || fromElement or toElement is not within the domain of the SortedSet *);
signals (java.lang.NullPointerException) (fromElement == null||toElement == null)&&!this.containsNull;

headSet

public SortedSet headSet(Object toElement)

Specifications: (class)pure

public behavior
ensures (\result .firstElement.equals(this.firstElement));
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(toElement) is incompatible with with this set's comparator *);
signals (java.lang.IllegalArgumentException) (* toElement is not within the domain of the SortedSet *);
signals (java.lang.NullPointerException) toElement == null&&!this.containsNull;

tailSet

public SortedSet tailSet(Object fromElement)

Specifications: (class)pure

public behavior
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(fromElement) is incompatible with this set's comparator *);
signals (java.lang.IllegalArgumentException) (* fromKey is not within the domain of the SortedSet *);
signals (java.lang.NullPointerException) fromElement == null&&!this.containsNull;

first

public Object first()

Specifications: (class)pure

public behavior
ensures \result .equals(this.firstElement);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.theSet.isEmpty();

last

public Object last()

Specifications: (class)pure

public behavior
ensures \result .equals(this.lastElement);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.theSet.isEmpty();