JML

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
Method Detail

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))));

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.