| org.jmlspecs.models.JMLCollection
All known Subclasses: org.jmlspecs.models.JMLValueBag, org.jmlspecs.models.JMLEqualsBag, org.jmlspecs.models.JMLEqualsSet, org.jmlspecs.models.JMLEqualsToObjectRelation, org.jmlspecs.models.JMLObjectToEqualsRelation, org.jmlspecs.models.JMLObjectToObjectRelation, org.jmlspecs.models.JMLValueSet, org.jmlspecs.models.JMLEqualsToValueRelation, org.jmlspecs.models.JMLEqualsToEqualsRelation, org.jmlspecs.models.JMLValueToValueRelation, org.jmlspecs.models.JMLObjectBag, org.jmlspecs.models.JMLObjectSet, org.jmlspecs.models.JMLValueToObjectRelation, org.jmlspecs.models.JMLObjectToValueRelation, org.jmlspecs.models.JMLObjectSequence, org.jmlspecs.models.JMLValueToEqualsRelation, org.jmlspecs.models.JMLValueSequence, org.jmlspecs.models.JMLEqualsSequence,
| JMLCollection | | public interface JMLCollection extends JMLType(Code) | | Common protocol of the JML model collection types.
The use of elementType and containsNull in this specification
follows the ESC/Java specification of
java.util.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.1.1.1 $
author:
Gary T. Leavens
author:
Yoonsik Cheon
See Also: JMLEnumeration
See Also: 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. | | public int | int_size()
Tell the number of elements in this collection. | | JMLIterator | iterator()
Returns an Iterator over this object. |
| has | | boolean has(Object elem)(Code) | | 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()(Code) | | Tell the number of elements in this collection.
|
|
|