org.jmlspecs.models
Interface JMLCollection

All Superinterfaces:

Cloneable, JMLType, Serializable

All Known Implementing Classes:

JMLEqualsBag, JMLEqualsSequence, JMLEqualsSet, JMLEqualsToEqualsRelation, JMLEqualsToObjectRelation, JMLEqualsToValueRelation, JMLObjectBag, JMLObjectSequence, JMLObjectSet, JMLObjectToEqualsRelation, JMLObjectToObjectRelation, JMLObjectToValueRelation, JMLValueBag, JMLValueSequence, JMLValueSet, JMLValueToEqualsRelation, JMLValueToObjectRelation, JMLValueToValueRelation, StringOfObject

public interface JMLCollection

extends JMLType

Common protocol of the JML model collection types. The use of elementType and containsNull in this specification follows the ESC/Java specification of Collection. That is, these ghost fields are used by the user of the object to state what types of objects are allowed to be added to the collection, and hence what is guaranteed to be retrieved from the collection. They are not adjusted by methods based on the content of the collection.

Version:

$Revision: 1.11 $

Author:

Gary T. Leavens, Yoonsik Cheon

See Also:

JMLEnumeration, JMLIterator

Method Summary
boolean	has(Object elem)           Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.
int	int_size()           Tell the number of elements in this collection.
JMLIterator	iterator()           The type of the elements in this collection.

 

Methods inherited from interface org.jmlspecs.models.JMLType

clone, equals, hashCode

 

Method Detail

iterator

public JMLIterator iterator()

The type of the elements in this collection. Whether this collection can contain null elements; think of it as "is allowed to contain null". Returns an Iterator over this object.

has

public boolean has(Object elem)

Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.

int_size

public int int_size()

Tell the number of elements in this collection.