org.jmlspecs.samples.sets
Class IntegerSetAsHashSet

java.lang.Object
  org.jmlspecs.samples.sets.IntegerSetAsHashSet

All Implemented Interfaces:

IntegerSetInterface

public class IntegerSetAsHashSet

extends Object

implements IntegerSetInterface

A set of integers as a HashSet.

Author:

Katie Becker, Gary T. Leavens

Class Specifications

private represents theSet <- this.abstractValue();

Specifications inherited from class Object

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

Specifications inherited from interface IntegerSetInterface

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

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.sets.IntegerSetInterface

theSet

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
private  HashSet	hset

 

Constructor Summary

IntegerSetAsHashSet()           Initialize this set to be the empty set.

 

Model Method Summary
private  JMLValueSet	abstractValue()           Return the abstract value of this IntegerSetAsHashSet.

 

Model methods inherited from class java.lang.Object

hashValue

 

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

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

hset

private HashSet hset

Specifications: non_null
is in groups: theSet
maps hset.theSet \into theSet

IntegerSetAsHashSet

public IntegerSetAsHashSet()

Initialize this set to be the empty set.

Specifications:

public normal_behavior
assignable theSet;
ensures this.theSet != null&&this.theSet.isEmpty();

abstractValue

private JMLValueSet abstractValue()

Return the abstract value of this IntegerSetAsHashSet.

Specifications: pure

isMember

public boolean isMember(int i)

Description copied from interface: IntegerSetInterface

Tell if the argument is in this set.

Specified by:

isMember in interface IntegerSetInterface

Specifications: pure

Specifications inherited from overridden method isMember(int elem) in interface IntegerSetInterface:
       pure

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

insert

public void insert(int i)

Description copied from interface: IntegerSetInterface

Insert the given integer into this set.

Specified by:

insert in interface IntegerSetInterface

Specifications inherited from overridden method insert(int elem) in interface IntegerSetInterface:

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

remove

public void remove(int i)

Description copied from interface: IntegerSetInterface

Remove the given integer from this set.

Specified by:

remove in interface IntegerSetInterface

Specifications inherited from overridden method remove(int elem) in interface IntegerSetInterface:

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

toString

public String toString()

Overrides:

toString in class Object

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;