org.jmlspecs.samples.table
Class TableImplementation

java.lang.Object
  org.jmlspecs.samples.table.TableImplementation

All Implemented Interfaces:

Table

public class TableImplementation

extends Object

implements Table

An implementation of the Table interface.

Author:

Katie Becker, Gary T. Leavens

Class Specifications

private represents entries <- this.abstractValue();

Specifications inherited from class Object

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

Specifications inherited from interface Table

instance public invariant this.entries != null&&( \forall org.jmlspecs.models.JMLType e; this.entries.has(e); e instanceof org.jmlspecs.samples.table.Entry); instance public invariant ( \forall org.jmlspecs.samples.table.Entry e1; this.entries.has(e1); ( \forall org.jmlspecs.samples.table.Entry e2; this.entries.has(e2)&&!(e1.equals(e2)); !(e1.index.equals(e2.index)))); public initially this.entries != null&&this.entries.isEmpty();

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.table.Table

entries

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
private  Hashtable	table           The representation of this Table.

 

Constructor Summary

TableImplementation()           Initialize this Table to contain the empty set of entries.

 

Model Method Summary
JMLValueSet	abstractValue()           Return the set of entries that are, abstractly, in this Table.

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	addEntry(Entry e)           Add the given entry to this table.
boolean	isUsedIndex(JMLType d)           Is the given index used in the table?
JMLType	mapTo(JMLType d)           Return the value at the given index.
void	removeEntry(JMLType d)           Take out the given entry from this table.
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Field Detail

table

private Hashtable table

The representation of this Table.

Specifications: non_null
is in groups: entries
maps table.theMap \into entries

TableImplementation

public TableImplementation()

Initialize this Table to contain the empty set of entries.

Specifications:

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

    implies_that

private normal_behavior
assignable entries, table;
ensures this.table != null;

abstractValue

public JMLValueSet abstractValue()

Return the set of entries that are, abstractly, in this Table.

Specifications: pure

ensures \result != null;

isUsedIndex

public boolean isUsedIndex(JMLType d)

Description copied from interface: Table

Is the given index used in the table?

Specified by:

isUsedIndex in interface Table

Specifications: pure

Specifications inherited from overridden method isUsedIndex(JMLType d) in interface Table:
       pure

public normal_behavior
requires d != null;
ensures \result <==> ( \exists org.jmlspecs.samples.table.Entry e; this.entries.has(e)&&e != null; e.index.equals(d));

addEntry

public void addEntry(Entry e)

Description copied from interface: Table

Add the given entry to this table.

Specified by:

addEntry in interface Table

Specifications inherited from overridden method addEntry(Entry e) in interface Table:

public normal_behavior
requires e != null&&!this.isUsedIndex(e.index);
assignable entries;
ensures this.entries.equals(\old(this.entries.insert(e)));

removeEntry

public void removeEntry(JMLType d)

Description copied from interface: Table

Take out the given entry from this table.

Specified by:

removeEntry in interface Table

Specifications inherited from overridden method removeEntry(JMLType d) in interface Table:

public normal_behavior
requires d != null;
assignable entries;
ensures this.entries.equals( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.samples.table.Entry e | \old(this.entries).has(e) && e != null&&!(e.index.equals(d)) });

mapTo

public JMLType mapTo(JMLType d)

Description copied from interface: Table

Return the value at the given index.

Specified by:

mapTo in interface Table

Specifications inherited from overridden method mapTo(JMLType d) in interface Table:

public normal_behavior
requires this.isUsedIndex(d);
assignable entries;
ensures \fresh(\result )&&( \exists org.jmlspecs.samples.table.Entry e; this.entries.has(e); e.index.equals(d)&&\result .equals(e.value));

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;