JML

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

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

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.