JML

org.jmlspecs.lang
Interface JMLSetType


public interface JMLSetType

Common protocol for the JML set model types. This is put in org.jmlspecs.lang because the language creates sets using set comprehensions. It should also be useful for the runtime assertion checker and other tools, to know what it can count on from the JML set types.

Version:
$Revision: 1.2 $
Author:
Gary T. Leavens
See Also:
JMLCollection, JMLEqualsSet, JMLValueSet, JMLObjectSet

Method Summary
 Object choose()
          Return an arbitrary element of this.
 boolean equals(Object s2)
           
 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.
 JMLSetType insert(Object elem)
          Returns a new set that contains all the elements of this and also the given argument.
 int int_size()
          Tells the number of elements in the set.
 boolean isEmpty()
          Is the set empty.
 Object[] toArray()
          Return a new array containing all the elements of this.
 

Method Detail

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.


equals

public boolean equals(Object s2)

isEmpty

public boolean isEmpty()
Is the set empty.

See Also:
int_size(), has(Object)

int_size

public int int_size()
Tells the number of elements in the set.


choose

public Object choose()
Return an arbitrary element of this.

See Also:
isEmpty(), #elements()

insert

public JMLSetType insert(Object elem)
Returns a new set that contains all the elements of this and also the given argument.

See Also:
has(Object), #remove(Object)

toArray

public Object[] toArray()
Return a new array containing all the elements of this.


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.