org.jmlspecs.samples.jmlkluwer
Class QueueEntry

java.lang.Object
  org.jmlspecs.samples.jmlkluwer.QueueEntry

All Implemented Interfaces:

Cloneable, JMLType, Serializable

public class QueueEntry

extends Object

implements JMLType

Class Specifications

private invariant_redundantly this._priorityLevel >= 0&&this._timeStamp >= 0; public invariant this.priorityLevel >= 0&&this.timeStamp >= 0; private represents obj <- this._obj; private represents priorityLevel <- this._priorityLevel; private represents timeStamp <- this._timeStamp;

Specifications inherited from class Object

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

Model Field Summary
Object	obj
int	priorityLevel
long	timeStamp

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
private  Object	_obj
private  int	_priorityLevel
private  long	_timeStamp

 

Constructor Summary

QueueEntry(Object argObj, int argLevel, long argTimeStamp)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()           Return a clone of this object.
boolean	equals(nullable Object o)           Test whether this object's value is equal to the given argument.
int	getLevel()
Object	getObj()
int	hashCode()           Return a hash code for this object.
String	toString()

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Model Field Detail

obj

public Object obj

Specifications:
datagroup contains: _obj

priorityLevel

public int priorityLevel

Specifications:
datagroup contains: _priorityLevel

timeStamp

public long timeStamp

Specifications:
datagroup contains: _timeStamp

_obj

private Object _obj

Specifications: non_null
is in groups: obj

_priorityLevel

private int _priorityLevel

Specifications:
is in groups: priorityLevel

_timeStamp

private long _timeStamp

Specifications:
is in groups: timeStamp

QueueEntry

public QueueEntry(Object argObj,
                  int argLevel,
                  long argTimeStamp)

Specifications: (class)pure

public normal_behavior
requires argLevel >= 0&&argTimeStamp >= 0;
assignable obj, priorityLevel, timeStamp;
ensures this.obj == argObj&&this.priorityLevel == argLevel&&this.timeStamp == argTimeStamp;

equals

public boolean equals(nullable Object o)

Description copied from interface: JMLType

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

     also

public normal_behavior
old org.jmlspecs.samples.jmlkluwer.QueueEntry oldo = (org.jmlspecs.samples.jmlkluwer.QueueEntry)o;
requires o instanceof org.jmlspecs.samples.jmlkluwer.QueueEntry;
ensures \result <==> oldo.obj == this.obj&&oldo.priorityLevel == this.priorityLevel&&oldo.timeStamp == this.timeStamp;

     also

public normal_behavior
requires !(o instanceof org.jmlspecs.samples.jmlkluwer.QueueEntry);
ensures \result == false;

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

Description copied from interface: JMLType

Return a hash code for this object.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object

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

clone

public Object clone()

Description copied from interface: JMLType

Return a clone of this object.

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

Specifications: (class)pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.samples.jmlkluwer.QueueEntry;
ensures_redundantly this.equals(\result );

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

getLevel

public int getLevel()

Specifications: pure

ensures \result == this.priorityLevel;

getObj

public Object getObj()

Specifications: pure

ensures \result == this.obj;

toString

public String toString()

Overrides:

toString in class Object

Specifications: (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;