org.jmlspecs.samples.sets
Interface IntegerSetInterface

All Known Implementing Classes:

IntegerSetAsHashSet, IntegerSetAsTree

public interface IntegerSetInterface

Sets of integers.

Class Specifications

instance public invariant_redundantly this.theSet != null; instance public invariant ( \forall org.jmlspecs.models.JMLType e; this.theSet.has(e); e instanceof org.jmlspecs.models.JMLInteger); public initially this.theSet.isEmpty();

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLValueSet	theSet

 

Method Summary
void	insert(int elem)           Insert the given integer into this set.
boolean	isMember(int elem)           Tell if the argument is in this set.
void	remove(int elem)           Remove the given integer from this set.

 

Model Field Detail

theSet

public JMLValueSet theSet

Specifications: instance
datagroup contains: org.jmlspecs.samples.sets.IntegerSetAsHashSet.hset hset.theSet org.jmlspecs.samples.sets.IntegerSetAsTree.isEmpty org.jmlspecs.samples.sets.IntegerSetAsTree.rootValue org.jmlspecs.samples.sets.IntegerSetAsTree.left left.theSet org.jmlspecs.samples.sets.IntegerSetAsTree.right right.theSet org.jmlspecs.samples.sets.IntegerSetAsTree.parent

insert

public void insert(int elem)

Insert the given integer into this set.

Specifications:

public normal_behavior
assignable theSet;
ensures this.theSet.equals(\old(this.theSet.insert(new org.jmlspecs.models.JMLInteger(elem))));

isMember

public boolean isMember(int elem)

Tell if the argument is in this set.

Specifications: pure

public normal_behavior
ensures \result == this.theSet.has(new org.jmlspecs.models.JMLInteger(elem));

remove

public void remove(int elem)

Remove the given integer from this set.

Specifications:

public normal_behavior
assignable theSet;
ensures this.theSet.equals(\old(this.theSet.remove(new org.jmlspecs.models.JMLInteger(elem))));