java.util
Interface SortedMap

All Superinterfaces:

Map

All Known Implementing Classes:

TreeMap

public interface SortedMap

extends Map

JML's specification of java.util.SortedMap.

Version:

$Revision: 1.11 $

Author:

Katie Becker

Class Specifications

Specifications inherited from class Object

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

Specifications inherited from interface Map

axiom ( \forall java.util.Map m; ; ( \forall java.lang.Object k, v, vv; ; (m.contains(k,v)&&m.contains(k,vv)) ==> nullequals(v,vv))); instance public invariant ( \forall java.lang.Object o; this.theMap.has(o); o instanceof java.util.Map.Entry); instance public invariant ( \forall java.lang.Object o1, o2; this.theMap.has(o1)&&this.theMap.has(o2); o2 != o1 ==> !org.jmlspecs.models.JMLNullSafe.equals(o2,o1));

Model Field Summary
[instance]  JMLType	firstKey
[instance]  JMLType	lastKey

 

Model fields inherited from interface java.util.Map

theMap

 

Ghost Field Summary

 

Ghost fields inherited from interface java.util.Map

containsNull

 

Model Method Summary

 

Model methods inherited from interface java.util.Map

contains, contains, nullequals

 

Method Summary
Comparator	comparator()
Object	firstKey()
SortedMap	headMap(Object toKey)
Object	lastKey()
SortedMap	subMap(Object fromKey, Object toKey)
SortedMap	tailMap(Object fromKey)

 

Methods inherited from interface java.util.Map

clear, containsKey, containsValue, entrySet, equals, get, hashCode, isEmpty, keySet, put, putAll, remove, size, values

 

Model Field Detail

firstKey

public JMLType firstKey

Specifications: instance
is in groups: theMap

lastKey

public JMLType lastKey

Specifications: instance
is in groups: theMap

comparator

public Comparator comparator()

Specifications: pure

public normal_behavior
ensures true;

subMap

public SortedMap subMap(Object fromKey,
                        Object toKey)

Specifications: pure

public behavior
assignable \nothing;
ensures (\result .firstKey.equals(this.firstKey));
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(fromKey) or \typeof(toKey) is incompatible with this map's comparator *);
signals (java.lang.IllegalArgumentException) (* fromKey > toKey || fromKey or toKey is not within the domain of the SortedMap *);
signals (java.lang.NullPointerException) (fromKey == null||toKey == null)&&!this.containsNull;

headMap

public SortedMap headMap(Object toKey)

Specifications: pure

public behavior
assignable \nothing;
ensures (\result .firstKey.equals(this.firstKey));
ensures \result != null;
signals_only java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(toKey) is incompatible with with this map's comparator *);
signals (java.lang.IllegalArgumentException) (* toKey is not within the domain of the SortedMap *);
signals (java.lang.NullPointerException) toKey == null&&!this.containsNull;

tailMap

public SortedMap tailMap(Object fromKey)

Specifications: pure

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

firstKey

public Object firstKey()

Specifications: pure

public behavior
assignable \nothing;
ensures \result .equals(this.firstKey);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.isEmpty();

lastKey

public Object lastKey()

Specifications: pure

public behavior
assignable \nothing;
ensures \result .equals(this.lastKey);
signals_only java.util.NoSuchElementException;
signals (java.util.NoSuchElementException) this.isEmpty();