Object (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

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.

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

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

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.

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.

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

java.lang Class Object

objectState

_getClass

theString

owner

objectTimesFinalized

Object

hashValue

getClass

hashCode

equals

clone

toString

notify

notifyAll

wait

wait

wait

finalize

java.lang
Class Object