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

Class Specifications

instance public constraint this.elementType == \old(this.elementType); instance public constraint this.containsNull == \old(this.containsNull);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  JMLDataGroup	elementState           The objectState of all elements is contained in elementState.

 

Ghost Field Summary
[instance]  boolean	containsNull           Whether this collection can contain null elements; think of it as "is allowed to contain null".
[instance]  Class	elementType           The type of the elements in this collection.

 

Model Method Summary
\bigint	size()           Tell the number of elements in this collection.

 

Method Summary
boolean	has(nullable 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()
JMLIterator	iterator()           Returns an Iterator over this object.

 

Methods inherited from interface org.jmlspecs.models.JMLType

clone, equals, hashCode

 

Model Field Detail

elementState

public JMLDataGroup elementState

The objectState of all elements is contained in elementState.

Specifications: instance
datagroup contains: the_list.elementState the_list.elementState theSeq.elementState the_list.elementState the_list.elementState theSeq.elementState theSeq.elementState the_list.elementState the_list.elementState

elementType

public Class elementType

The type of the elements in this collection.

Specifications: instance

containsNull

public boolean containsNull

Whether this collection can contain null elements; think of it as "is allowed to contain null".

Specifications: instance

size

public \bigint size()

Tell the number of elements in this collection.

Specifications: pure

public normal_behavior
ensures \result >= 0&&(* \result is the size of this collection *);

iterator

public JMLIterator iterator()

Returns an Iterator over this object.

Specifications: pure non_null

public normal_behavior
ensures \fresh(\result )&&\result .elementType == this.elementType;
ensures !this.containsNull ==> !\result .returnsNull;

has

public boolean has(nullable 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.

Specifications: pure

public normal_behavior
ensures (* \result <==> elem is equal to one of the elements in the collection. *);
ensures_redundantly !this.containsNull&&elem == null ==> !\result ;
ensures_redundantly elem != null&&!(\typeof(elem) <: this.elementType) ==> !\result ;

int_size

public int int_size()

Specifications: pure

public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();