JML

org.jmlspecs.models
Class JMLValueBagEntry

java.lang.Object
  extended byorg.jmlspecs.models.JMLValueBagEntry
All Implemented Interfaces:
Cloneable, JMLType, Serializable

class JMLValueBagEntry
extends Object
implements JMLType

Internal class used in the implementation of JMLValueBag.

Author:
Gary T. Leavens
See Also:
JMLValueBag, JMLValueBagEntryNode

Class Specifications
public invariant this.count > 0;
public invariant this.elementType <: \type(org.jmlspecs.models.JMLType);
public invariant (this.theElem == null ==> this.elementType == \type(org.jmlspecs.models.JMLType))&&(this.theElem != null ==> this.elementType == \typeof(this.theElem));
public invariant this.owner == null;

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
 Class elementType
          The type of the element in this entry.
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
 int count
          The number of times the element occurs.
 JMLType theElem
          The element in this bag entry.
 
Constructor Summary
JMLValueBagEntry(JMLType e)
          Initialize this object to be a singleton entry.
JMLValueBagEntry(JMLType e, int cnt)
          Initialize this object to be for the given element with the given number of repetitions.
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
          Make a clone of the given entry.
 boolean equalElem(JMLType othElem)
          Are these elements equal?
 boolean equals(nullable Object obj)
          Test whether this object's value is equal to the given argument.
 int hashCode()
          Return a hash code for this object.
 JMLValueBagEntry insert(int numInserted)
          Return a new bag entry with the same element as this but with the given number of repetitions added to the element's current count.
 String toString()
          Return a string representation of this object.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Ghost Field Detail

elementType

public Class elementType
The type of the element in this entry. This is JMLType if the element is null.

Field Detail

theElem

public final JMLType theElem
The element in this bag entry.


count

public final int count
The number of times the element occurs.

Constructor Detail

JMLValueBagEntry

public JMLValueBagEntry(JMLType e)
Initialize this object to be a singleton entry.

Specifications: (class)pure
public normal_behavior
assignable theElem, count, elementType, owner;
ensures this.theElem == e&&this.count == 1;

JMLValueBagEntry

public JMLValueBagEntry(JMLType e,
                        int cnt)
Initialize this object to be for the given element with the given number of repetitions.

Specifications: (class)pure
public normal_behavior
requires cnt > 0;
assignable theElem, count, elementType, owner;
ensures this.count == cnt&&(e == null ==> this.theElem == null);
ensures (e != null ==> e.equals(this.theElem));
Method Detail

clone

public Object clone()
Make a clone of the given entry.

Specified by:
clone in interface JMLType
Overrides:
clone in class Object
Specifications: non_null (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 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);

equalElem

public boolean equalElem(JMLType othElem)
Are these elements equal?

Specifications: (class)pure
public normal_behavior
ensures \result <==> (othElem == null&&this.theElem == null)||(othElem != null&&othElem.equals(this.theElem));

equals

public boolean equals(nullable Object obj)
Test whether this object's value is equal to the given argument.

Specified by:
equals in interface JMLType
Overrides:
equals in class Object
Specifications: (class)pure
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;
Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure
     also
public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);
    implies_that
public normal_behavior
{|
requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;
also
requires ob2 == this;
ensures \result <==> true;
|}

hashCode

public int hashCode()
Return a hash code for this object.

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object
Specifications: (class)pure
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;
Specifications inherited from overridden method in interface JMLType:
       pure

insert

public JMLValueBagEntry insert(int numInserted)
Return a new bag entry with the same element as this but with the given number of repetitions added to the element's current count.

Specifications: (class)pure
public normal_behavior
requires numInserted > 0;
ensures \result != null&&\result .count == this.count+numInserted;
ensures \result != null&&\result .theElem.equals(this.theElem);

toString

public String toString()
Return a string representation of this object.

Overrides:
toString in class Object
Specifications: non_null (class)pure
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;

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.