JML

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
Method Detail

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();

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.