org.jmlspecs.models
Class JMLValueBagSpecs

java.lang.Object
  org.jmlspecs.models.JMLValueBagSpecs

All Implemented Interfaces:

Cloneable, JMLType, JMLValueType, Serializable

Direct Known Subclasses:

JMLValueBag

public abstract class JMLValueBagSpecs

extends Object

implements JMLValueType

Special behavior for JMLValueBag not shared by JMLObjectBag.

Version:

$Revision: 1.18 $

Author:

Gary T. Leavens, with help from Clyde Ruby, and others.

See Also:

JMLValueType, JMLValueBag

Class Specifications

Specifications inherited from class Object

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

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

JMLValueBagSpecs()

 

Model Method Summary
int	countObject(JMLType elem)           How many times does the argument occur as an objects representing values in the bag?

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
abstract  Object	clone()           Return a deep copy of this object.
int	count(nullable Object elem)           Tell many times the argument occurs ".equals" to one of the values in this bag.
abstract  int	count(nullable JMLType elem)           Tell many times the argument occurs ".equals" to one of the values in this bag.
boolean	has(nullable Object elem)           Is the argument ".equals" to one of the values in this bag.
abstract  boolean	has(nullable JMLType elem)           Is the argument ".equals" to one of the values in this bag.
abstract  JMLValueBag	insert(nullable JMLType elem, int cnt)
abstract  int	int_size()           Tells the number of elements in the bag.

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.jmlspecs.models.JMLValueType

equals

 

Methods inherited from interface org.jmlspecs.models.JMLType

hashCode

 

Constructor Detail

JMLValueBagSpecs

public JMLValueBagSpecs()

countObject

public int countObject(JMLType elem)

How many times does the argument occur as an objects representing values in the bag?

See Also:

count(Object)

Specifications: (class)pure

public normal_behavior
ensures (* \result is the number of occurences of objects in this bag that are "==" to elem *);

has

public abstract boolean has(nullable JMLType elem)

Is the argument ".equals" to one of the values in this bag.

See Also:

has(Object), count(JMLType)

Specifications: (class)pure

public normal_behavior
ensures \result <==> this.count(elem) > 0;

has

public boolean has(nullable Object elem)

Is the argument ".equals" to one of the values in this bag.

See Also:

has(JMLType), count(Object)

Specifications: (class)pure

public normal_behavior
requires elem != null;
ensures \result <==> elem instanceof org.jmlspecs.models.JMLType&&this.has((org.jmlspecs.models.JMLType)elem);

     also

public normal_behavior
requires elem == null;
ensures \result == this.has(null);

count

public abstract int count(nullable JMLType elem)

Tell many times the argument occurs ".equals" to one of the values in this bag.

See Also:

count(Object), has(JMLType)

Specifications: (class)pure

public normal_behavior
ensures \result >= 0&&(* \result is the number of times elem tests as ".equals" to one of the objects in the bag *);

count

public int count(nullable Object elem)

Tell many times the argument occurs ".equals" to one of the values in this bag.

See Also:

count(JMLType), has(Object)

Specifications: (class)pure

public normal_behavior
requires elem != null;
ensures \result == (elem instanceof org.jmlspecs.models.JMLType ? this.count((org.jmlspecs.models.JMLType)elem) : 0);

     also

public normal_behavior
requires elem == null;
ensures \result == this.count(null);

int_size

public abstract int int_size()

Tells the number of elements in the bag.

Specifications: (class)pure

public normal_behavior
ensures \result >= 0&&(* \result is the number of elements in the bag *);

clone

public abstract Object clone()

Description copied from interface: JMLValueType

Return a deep copy of this object.

Specified by:

clone in interface JMLValueType

Overrides:

clone in class Object

Specifications: (class)pure

Specifications inherited from overridden method in class Object:
       non_null

protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);

     also

protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));

     also

protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;

     also

protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

Specifications inherited from overridden method in interface JMLValueType:
       pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueType&&(* all externally-visible mutable objects contained directly in "this" must be cloned in \result. *);

    implies_that

ensures (* no direct aliases are created between this and \result *);

Specifications inherited from overridden method in interface JMLType:
       pure

     also

public normal_behavior
ensures \result != null;
ensures \result instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)\result ).equals(this);

    implies_that

ensures \result != null&&\typeof(\result ) <: \type(org.jmlspecs.models.JMLType);

insert

public abstract JMLValueBag insert(nullable JMLType elem,
                                   int cnt)
                            throws IllegalArgumentException,
                                   IllegalStateException

Throws:

IllegalArgumentException

IllegalStateException

Specifications: non_null (class)pure

public model_program { ... }

     also

signals (java.lang.IllegalArgumentException) cnt < 0;