JML

java.lang
Class Object

java.lang.Object

public class Object

JML's specification of java.lang.Object.

Version:
$Revision: 1.56 $
Author:
Gary T. Leavens, Specifications from Compaq SRC's ESC/Java

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

Model Field Summary
 Class _getClass
          The Class of this object.
 JMLDataGroup objectState
          A data group for the state of this object.
 String theString
          Use theString as the (pure) model value of toString()
 
Ghost Field Summary
protected  int objectTimesFinalized
          The number of times this object has been finalized.
 Object owner
          The Object that has a field pointing to this Object.
 
Constructor Summary
Object()
           
 
Model Method Summary
 int hashValue()
           
 
Method Summary
protected  Object clone()
           
 boolean equals(nullable Object obj)
           
protected  void finalize()
           
 Class getClass()
           
 int hashCode()
           
 void notify()
           
 void notifyAll()
           
 String toString()
           
 void wait()
           
 void wait(long timeout)
           
 void wait(long timeout, int nanos)
           
 

Model Field Detail

objectState

public JMLDataGroup objectState
A data group for the state of this object. This is used to allow side effects on unknown variables in methods such as equals, clone, and toString. It also provides a convenient way to talk about "the state" of an object in assignable clauses.

Specifications: non_null
datagroup contains: java.util.Iterator.moreElements java.util.ListIterator.cursor_position java.util.Map.theMap java.util.Enumeration.moreElements java.io.DataInput.input org.jmlspecs.checker.JmlMethodName.stringRepresentation org.jmlspecs.checker.JmlMethodNameList.stringRepresentation org.jmlspecs.models.JMLValueSequenceEnumerator.uniteratedElems org.jmlspecs.models.JMLValueToValueRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectToObjectRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLEqualsSequenceEnumerator.uniteratedElems org.jmlspecs.models.JMLValueBagEnumerator.uniteratedElems org.jmlspecs.models.JMLObjectBagEnumerator.uniteratedElems org.jmlspecs.models.JMLObjectToEqualsRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLObjectToValueRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectToEqualsRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectToObjectRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLValueSet.the_list org.jmlspecs.models.JMLValueSet.size org.jmlspecs.models.JMLValueToValueRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLEqualsSetEnumerator.uniteratedElems org.jmlspecs.models.JMLEqualsToObjectRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectToValueRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLValueSetEnumerator.uniteratedElems org.jmlspecs.models.JMLEqualsBag.the_list org.jmlspecs.models.JMLEqualsBag.size org.jmlspecs.models.JMLListEqualsNode.val org.jmlspecs.models.JMLListEqualsNode.next org.jmlspecs.models.JMLListObjectNode.val org.jmlspecs.models.JMLListObjectNode.next org.jmlspecs.models.JMLValueToEqualsRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLEqualsToEqualsRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLListValueNode.val org.jmlspecs.models.JMLListValueNode.next org.jmlspecs.models.JMLEqualsSequence.theSeq org.jmlspecs.models.JMLEqualsSequence._length org.jmlspecs.models.JMLEqualsBagEnumerator.uniteratedElems org.jmlspecs.models.JMLEqualsToEqualsRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLValueBag.the_list org.jmlspecs.models.JMLValueBag.size org.jmlspecs.models.JMLEqualsToObjectRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLObjectBag.the_list org.jmlspecs.models.JMLObjectBag.size org.jmlspecs.models.JMLEqualsToValueRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLObjectSequence.theSeq org.jmlspecs.models.JMLObjectSequence._length org.jmlspecs.models.JMLValueSequence.theSeq org.jmlspecs.models.JMLValueSequence._length org.jmlspecs.models.JMLEqualsSet.the_list org.jmlspecs.models.JMLEqualsSet.size org.jmlspecs.models.JMLValueToObjectRelationImageEnumerator.uniteratedImagePairs org.jmlspecs.models.JMLObjectSetEnumerator.uniteratedElems org.jmlspecs.models.JMLValueToObjectRelationEnumerator.uniteratedPairs theEnumeration.objectState org.jmlspecs.models.JMLEqualsToValueRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectSet.the_list org.jmlspecs.models.JMLObjectSet.size org.jmlspecs.models.JMLValueToEqualsRelationEnumerator.uniteratedPairs org.jmlspecs.models.JMLObjectSequenceEnumerator.uniteratedElems org.jmlspecs.models.resolve.StringOfObject.elements org.jmlspecs.models.resolve.NaturalNumber.value org.jmlspecs.jmlunit.TestClassGenerator$MethodsIterator.methods methods.objectState org.jmlspecs.jmlunit.TestClassGenerator$MethodsIterator.inheritedMethods inheritedMethods.objectState org.jmlspecs.jmlunit.TestClassGenerator$MethodsIterator.cache org.jmlspecs.jmlunit.FancyTabbedPrintWriter.writer writer.objectState org.jmlspecs.jmlunit.strategies.LongCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.LongCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.LongAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.AbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.AbstractExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.AbstractExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.CharArrayIterator.next org.jmlspecs.jmlunit.strategies.CompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.CompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.DoubleCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.IntExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.ShortAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.CharCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.CharCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.DoubleAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.BooleanExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.BooleanExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.LongExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.LongExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.BooleanAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.ByteAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.ByteExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.CharExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.CharExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.FloatArrayIterator.next org.jmlspecs.jmlunit.strategies.LongArrayIterator.next org.jmlspecs.jmlunit.strategies.ByteAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.LongExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.ByteCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.IntExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.IntExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.FloatExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.FloatExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.NewObjectAbstractExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.NewObjectAbstractExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.ShortCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.FloatAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.ShortExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.ShortExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.DoubleAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.ByteArrayIterator.next org.jmlspecs.jmlunit.strategies.ShortCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.ShortCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.CharAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.FloatExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.CompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.LongAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.IntAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.ByteExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.ByteExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.ShortAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.FloatAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.BooleanCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.NewObjectAbstractIterator.atEnd org.jmlspecs.jmlunit.strategies.NewObjectAbstractIterator.cursor org.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator.next org.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator.elems org.jmlspecs.jmlunit.strategies.ShortArrayIterator.next org.jmlspecs.jmlunit.strategies.CharAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.LongCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.IntCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.IntCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.AbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.DoubleExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.CharCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.DoubleCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.DoubleCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.DoubleArrayIterator.next org.jmlspecs.jmlunit.strategies.IntAbstractFilteringIteratorDecorator.rawElems rawElems.objectState org.jmlspecs.jmlunit.strategies.DoubleExtensibleStrategyDecorator.defaultData defaultData.objectState org.jmlspecs.jmlunit.strategies.DoubleExtensibleStrategyDecorator.addedData addedData.objectState org.jmlspecs.jmlunit.strategies.IteratorAbstractAdapter.atEnd org.jmlspecs.jmlunit.strategies.IteratorAbstractAdapter.item org.jmlspecs.jmlunit.strategies.FloatCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.FloatCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.CachedObjectAbstractStrategy.data org.jmlspecs.jmlunit.strategies.ShortExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.BooleanExtensibleStrategy.data org.jmlspecs.jmlunit.strategies.BooleanArrayIterator.next org.jmlspecs.jmlunit.strategies.BooleanCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.BooleanCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.FloatCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.IntCompositeStrategy.strats strats[*].objectState org.jmlspecs.jmlunit.strategies.BooleanAbstractFilteringStrategyDecorator.rawData rawData.objectState org.jmlspecs.jmlunit.strategies.ByteCompositeIterator.currentIterator org.jmlspecs.jmlunit.strategies.ByteCompositeIterator.iters iters[*].objectState org.jmlspecs.jmlunit.strategies.IntArrayIterator.next org.jmlspecs.jmlunit.strategies.CharExtensibleStrategy.data java.lang.Throwable._message java.lang.Throwable._cause java.lang.Throwable._stackTrace owner java.io.InputStream.input java.io.InputStream._markSupported java.io.InputStream.markPosition java.io.InputStream.markLimit java.io.OutputStream.output java.io.OutputStream.isOpen java.io.OutputStream.wasClosed org.multijava.launcher.Launcher$ToolIterator.currentIndex org.multijava.mjc.CMethod.cachedPure org.multijava.mjc.CMethod.pureCached org.multijava.mjc.CMethod.purityWasChanged org.multijava.mjc.CVariableState.maybeAssigned org.multijava.mjc.CVariableState.isDefinitelyAssigned org.multijava.mjc.CVariableState.variableDesc org.multijava.mjc.CContext.parent parent.objectState org.multijava.mjc.CMethodContext.self self.objectState org.multijava.mjc.CClassType.thisClassInfo org.multijava.util.testing.FileIterator.r org.multijava.util.testing.FileIterator.nextLine org.multijava.util.testing.ExternalInputIterator.pp org.multijava.util.testing.ExternalInputIterator.r org.multijava.util.testing.ExternalInputIterator.nextLine

_getClass

public Class _getClass
The Class of this object. Needed to specify that invoking getClass() on an object always produces the same result: no methods include this model field in their assignable clause, so no methods can alter the outcome of invoking getClass() on some object. This property is important when using ESC/Java on specs that use getClass(), just knowing that getClass() is pure is not enough.

Specifications: non_null

theString

public String theString
Use theString as the (pure) model value of toString()

Ghost Field Detail

owner

public Object owner
The Object that has a field pointing to this Object. Used to specify (among other things) injectivity (see the ESC/Java User's Manual).

Specifications: nullable
is in groups: objectState

objectTimesFinalized

protected int objectTimesFinalized
The number of times this object has been finalized.

Constructor Detail

Object

public Object()
Specifications: pure
public normal_behavior
assignable \nothing;
Model Method Detail

hashValue

public int hashValue()
Specifications: pure
Method Detail

getClass

public final Class getClass()
Specifications: pure non_null
public normal_behavior
ensures \result == this._getClass;
ensures_redundantly \result != null;

hashCode

public int hashCode()
Specifications:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;

equals

public boolean equals(nullable Object obj)
Specifications: 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 ;

clone

protected Object clone()
                throws CloneNotSupportedException
Throws:
CloneNotSupportedException
Specifications: 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]);

toString

public String toString()
Specifications: 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;

notify

public final void notify()

notifyAll

public final void notifyAll()

wait

public final void wait(long timeout)
                throws InterruptedException
Throws:
InterruptedException
Specifications:
requires timeout >= 0;

wait

public final void wait(long timeout,
                       int nanos)
                throws InterruptedException
Throws:
InterruptedException
Specifications:
requires timeout >= 0&&0 <= nanos&&nanos < 1000000;

wait

public final void wait()
                throws InterruptedException
Throws:
InterruptedException

finalize

protected void finalize()
                 throws Throwable
Throws:
Throwable
Specifications:
protected behavior
requires this.objectTimesFinalized == 0;
assignable objectTimesFinalized, objectState;
ensures this.objectTimesFinalized == 1;
signals (java.lang.Exception) this.objectTimesFinalized == 1;

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.