org.jmlspecs.samples.table
Interface Table

All Known Implementing Classes:

TableImplementation

public interface Table

Tables are finite maps from indexes to values.

Author:

Gary T. Leavens, Albert L. Baker

Class Specifications

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

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLValueSet	entries           The model of the entries (rows) in the table.

 

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.

 

Model Field Detail

entries

public JMLValueSet entries

The model of the entries (rows) in the table.

Specifications: instance
datagroup contains: org.jmlspecs.samples.table.TableImplementation.table table.theMap

isUsedIndex

public boolean isUsedIndex(JMLType d)

Is the given index used in the table?

Specifications: 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)

Add the given entry to this table.

Specifications:

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)

Take out the given entry from this table.

Specifications:

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)

Return the value at the given index.

Specifications:

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