JML

java.util
Interface Collection

All Known Subinterfaces:
List, Set, SortedSet
All Known Implementing Classes:
AbstractCollection, AbstractList, AbstractSet, ArrayList, HashSet, LinkedHashSet, LinkedList, TreeSet, Vector

public interface Collection

JML's specification of java.util.Collection. Part of this specification is adapted from ESC/Java.

Version:
$Revision: 1.33 $
Author:
Gary T. Leavens, Brandon Shilling

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

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  boolean addOperationSupported
           
[instance]  JMLDataGroup elementState
          The objectState of all elements is contained in elementState.
[instance]  boolean nullElementsSupported
           
[instance]  boolean removeOperationSupported
           
[instance]  JMLEqualsBag theCollection
           
 
Ghost Field Summary
[instance]  boolean containsNull
          True iff we are allowed to contain null (not whether we do in fact contain null).
[instance]  Class elementType
          The (more specific) type of our elements (set by the user of the object to state what is allowed to be added to the collection, and hence what is guaranteed to be retrieved from the collection).
 
Model Method Summary
 int hashValue()
           
 
Method Summary
 boolean add(nullable Object o)
           
 boolean addAll(Collection c)
           
 void clear()
           
 boolean contains(nullable Object o)
           
 boolean containsAll(Collection c)
           
 boolean equals(nullable Object o)
           
 int hashCode()
           
 boolean isEmpty()
           
 Iterator iterator()
           
 boolean remove(nullable Object o)
           
 boolean removeAll(Collection c)
           
 boolean retainAll(Collection c)
           
 int size()
           
 Object[] toArray()
           
 Object[] toArray(Object[] a)
           
 

Model Field Detail

elementState

public JMLDataGroup elementState
The objectState of all elements is contained in elementState.

Specifications: instance

theCollection

public JMLEqualsBag theCollection
Specifications: instance non_null
datagroup contains: java.util.Set.theSet java.util.List.theList

addOperationSupported

public boolean addOperationSupported
Specifications: instance

removeOperationSupported

public boolean removeOperationSupported
Specifications: instance

nullElementsSupported

public boolean nullElementsSupported
Specifications: instance
Ghost Field Detail

elementType

public Class elementType
The (more specific) type of our elements (set by the user of the object to state what is allowed to be added to the collection, and hence what is guaranteed to be retrieved from the collection). It is not adjusted based on the content of the collection.

Specifications: instance

containsNull

public boolean containsNull
True iff we are allowed to contain null (not whether we do in fact contain null).

Specifications: instance
Model Method Detail

hashValue

public int hashValue()
Overrides:
hashValue in class Object
Specifications: (inherited)pure
Specifications inherited from overridden method in class Object:
       pure
Method Detail

size

public int size()
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result == this.theCollection.int_size();
ensures \result >= 0;

isEmpty

public boolean isEmpty()
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result <==> this.theCollection.isEmpty();
     also
public normal_behavior
ensures \result == (this.size() == 0);

contains

public boolean contains(nullable Object o)
Specifications: pure
public behavior
assignable \nothing;
ensures !this.containsNull&&o == null ==> !\result ;
ensures (o == null)||\typeof(o) <: this.elementType||!\result ;
ensures \result <==> this.theCollection.has(o);
signals_only java.lang.ClassCastException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* \typeof(o) is incompatible with the elementType of this collection *);
signals (java.lang.NullPointerException) o == null;

iterator

public Iterator iterator()
Specifications: pure non_null
public normal_behavior
assignable \nothing;
ensures \result != null;
ensures \result .elementType == this.elementType;
ensures this.containsNull == \result .returnsNull;
     also
public normal_behavior
ensures ( \forall int i; 0 <= i&&i < this.size(); this.theCollection.has(\result .nthNextElement(i)));
ensures ( \forall java.lang.Object o; ; this.theCollection.has(o) ==> ( \exists int i; 0 <= i&&i < this.size(); o.equals(\result .nthNextElement(i))));
ensures this.size() > 0 ==> \result .hasNext((int)(this.size()-1));
ensures !\result .hasNext((int)(this.size()));
ensures_redundantly ( \forall int i; 0 <= i&&i < this.size(); this.contains(\result .nthNextElement(i)));
ensures_redundantly this.size() != 0 ==> \result .moreElements;

toArray

public Object[] toArray()
Specifications: pure non_null
public normal_behavior
requires this.size() < 2147483647;
assignable \nothing;
ensures \result != null;
ensures this.containsNull||\nonnullelements(\result );
ensures \result .length == this.size();
     also
public normal_behavior
ensures ( \forall int i; 0 <= i&&i < this.size(); this.theCollection.count(\result [i]) == org.jmlspecs.models.JMLArrayOps.valueEqualsCount(\result ,\result [i]));

toArray

public Object[] toArray(Object[] a)
Specifications: non_null
public normal_behavior
old int colSize = this.theCollection.int_size();
old int arrSize = a.length;
requires a != null&&colSize < 2147483647;
requires this.elementType <: \elemtype(\typeof(a));
requires ( \forall java.lang.Object o; this.contains(o); \typeof(o) <: \elemtype(\typeof(a)));
{|
requires colSize <= arrSize;
assignable a[*];
ensures \result == a;
ensures ( \forall int k; 0 <= k&&k < colSize; this.theCollection.count(\result [k]) == org.jmlspecs.models.JMLArrayOps.valueEqualsCount(\result ,\result [k],colSize));
ensures ( \forall int i; colSize <= i&&i < arrSize; \result [i] == null);
ensures_redundantly \typeof(\result ) == \typeof(a);
also
requires colSize > arrSize;
assignable \nothing;
ensures \fresh(\result )&&\result .length == colSize;
ensures ( \forall int k; 0 <= k&&k < colSize; this.theCollection.count(\result [k]) == org.jmlspecs.models.JMLArrayOps.valueEqualsCount(\result ,\result [k],colSize));
ensures ( \forall int k; 0 <= k&&k < colSize; \result [k] == null||\typeof(\result [k]) <: \elemtype(\typeof(\result )));
ensures \typeof(\result ) == \typeof(a);
|}
     also
public exceptional_behavior
requires a == null;
assignable \nothing;
signals_only java.lang.NullPointerException;
     also
public behavior
requires a != null;
requires !( \forall java.lang.Object o; o != null&&this.contains(o); \typeof(o) <: \elemtype(\typeof(a)));
assignable a[*];
signals_only java.lang.ArrayStoreException;

add

public boolean add(nullable Object o)
Specifications:
public behavior
requires !this.containsNull ==> o != null;
requires (o == null)||\typeof(o) <: this.elementType;
assignable theCollection;
ensures \result ==> this.theCollection.equals(\old(this.theCollection.insert(o)));
ensures \result &&\old(this.size() < 2147483647) ==> this.size() == \old(this.size()+1);
ensures !\result ==> this.size() == \old(this.size());
ensures !\result ==> \not_modified(theCollection);
ensures this.contains(o);
ensures_redundantly !\result ==> \old(this.contains(o));
signals_only java.lang.UnsupportedOperationException, java.lang.NullPointerException, java.lang.ClassCastException, java.lang.IllegalArgumentException;
signals (java.lang.UnsupportedOperationException) (* this does not support add *);
signals (java.lang.NullPointerException) (* not allowed to add null *);
signals (java.lang.ClassCastException) (* class of specified element prevents it from being added to this *);
signals (java.lang.IllegalArgumentException) (* some aspect of this element prevents it from being added to this *);

remove

public boolean remove(nullable Object o)
Specifications:
public behavior
requires !this.containsNull ==> o != null;
requires (o == null)||\typeof(o) <: this.elementType;
assignable theCollection;
ensures \result ==> this.theCollection.equals(\old(this.theCollection.remove(o)));
ensures \result &&\old(this.size() <= 2147483647) ==> this.size() == \old(this.size()-1)&&this.size() < 2147483647&&this.size() >= 0;
ensures !\result ||\old(this.size() == 2147483647) ==> this.size() == \old(this.size());
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException;
signals (java.lang.UnsupportedOperationException) (* this does not support remove *);
signals (java.lang.ClassCastException) (* the type of this element is not compatible with this *);

containsAll

public boolean containsAll(Collection c)
Specifications: pure
public behavior
requires c != null;
requires c.elementType <: this.elementType;
requires !this.containsNull ==> !c.containsNull;
assignable \nothing;
ensures \result <==> ( \forall java.lang.Object o; ; c.contains(o) ==> this.contains(o));
ensures \result <==> this.theCollection.containsAll(c);
signals_only java.lang.ClassCastException, java.lang.NullPointerException;
signals (java.lang.ClassCastException) (* class of specified element prevents it from being added to this *);
signals (java.lang.NullPointerException) (* argument contains null elements and this does not support null elements *);
     also
public exceptional_behavior
requires c == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

addAll

public boolean addAll(Collection c)
Specifications:
public behavior
requires c != null;
requires c.elementType <: this.elementType;
requires !this.containsNull ==> !c.containsNull;
assignable theCollection;
ensures this.theCollection.equals(\old(this.theCollection).union(c.theCollection));
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.NullPointerException;
signals (java.lang.UnsupportedOperationException) (* this does not support addAll *);
signals (java.lang.ClassCastException) (* class of specified element prevents it from being added to this *);
signals (java.lang.IllegalArgumentException) (* some aspect of this element prevents it from being added to this *);
signals (java.lang.NullPointerException) (* argument contains null elements and this does not support null elements *);
     also
public exceptional_behavior
requires c == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

removeAll

public boolean removeAll(Collection c)
Specifications:
public behavior
requires c != null;
requires this.elementType <: c.elementType;
requires !c.containsNull ==> !this.containsNull;
assignable theCollection;
ensures this.theCollection.equals(\old(this.theCollection).difference(c.theCollection));
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.NullPointerException;
signals (java.lang.UnsupportedOperationException) (* this does not support removeAll *);
signals (java.lang.ClassCastException) (* the type of one or more of the elements in c is not supported by this *);
signals (java.lang.NullPointerException) (* argument contains null elements and this does not support null elements *);
     also
public exceptional_behavior
requires c == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

retainAll

public boolean retainAll(Collection c)
Specifications:
public behavior
requires c != null;
requires this.elementType <: c.elementType;
requires !c.containsNull ==> !this.containsNull;
assignable theCollection;
ensures this.theCollection.equals(\old(this.theCollection).intersection(c.theCollection));
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.NullPointerException;
signals (java.lang.UnsupportedOperationException) (* this does not support retainAll *);
signals (java.lang.ClassCastException) (* the type of one or more of the elements in c is not supported by this *);
signals (java.lang.NullPointerException) (* argument contains null elements and this does not support null elements *);
     also
public exceptional_behavior
requires c == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

clear

public void clear()
Specifications:
public behavior
assignable theCollection;
ensures this.theCollection.isEmpty();
ensures_redundantly this.size() == 0;
signals_only java.lang.UnsupportedOperationException;
signals (java.lang.UnsupportedOperationException) (* clear is not supported by this *);

equals

public boolean equals(nullable Object o)
Overrides:
equals in class Object
Specifications: (inherited)pure
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;

hashCode

public int hashCode()
Overrides:
hashCode in class Object
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;

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.