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.