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

Class Specifications

Specifications inherited from class Object

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

Method Summary
Object	choose()           Return an arbitrary element of this.
boolean	equals(nullable 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.

Specifications: (class)pure

public normal_behavior
requires this.isEmpty();
ensures !\result ;

equals

public boolean equals(nullable Object s2)

Overrides:

equals in class Object

Specifications: (class)pure

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

isEmpty

public boolean isEmpty()

Is the set empty.

See Also:

int_size(), has(Object)

Specifications: (class)pure

public normal_behavior
ensures \result == ( \forall java.lang.Object e; ; !this.has(e));

int_size

public int int_size()

Tells the number of elements in the set.

Specifications: (class)pure

public normal_behavior
ensures this.isEmpty() ==> \result == 0;
ensures \result >= 0;

choose

public Object choose()

Return an arbitrary element of this.

See Also:

isEmpty(), #elements()

Specifications: (class)pure

public normal_behavior
requires !this.isEmpty();
ensures this.has(\result );

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)

Specifications: non_null (class)pure

public normal_behavior
requires this.int_size() < 2147483647||this.has(elem);
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) ==> this.has(e)||(e == null&&elem == null)||(e != null&&e.equals(elem)));

toArray

public Object[] toArray()

Return a new array containing all the elements of this.

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&\result .length == this.int_size()&&( \forall java.lang.Object o; this.has(o); ( \exists int i; ; (o == null&&\result [i] == null)||(o != null&&o.equals(\result [i]))));