JML

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.13 $
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 objectState of all elements is contained in elementState.
 
Methods inherited from interface org.jmlspecs.models.JMLType
clone, equals, hashCode
 

Method Detail

iterator

public JMLIterator iterator()
The objectState of all elements is contained in elementState. 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.


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.