001: package java.lang;
002:
003: import gnu.classpath.Configuration;
004:
005: public class Object {
006:
007: /** A data group for the state of this object. This is used to
008: * allow side effects on unknown variables in methods such as
009: * equals, clone, and toString. It also provides a convenient way
010: * to talk about "the state" of an object in assignable
011: * clauses.
012: */
013: //@ public non_null model org.jmlspecs.lang.JMLDataGroup objectState;
014: //@ represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
015: /** The Object that has a field pointing to this Object.
016: * Used to specify (among other things) injectivity (see
017: * the ESC/Java User's Manual).
018: */
019: /*@ ghost public Object owner;
020: @ in objectState;
021: @*/
022:
023: /** The number of times this object has been finalized.
024: */
025: //@ protected ghost int objectTimesFinalized;
026: /*@ public normal_behavior
027: @ assignable \nothing;
028: @*/
029: public/*@ pure @*/Object() {
030: }
031:
032: /*@
033: @ public normal_behavior
034: @ requires this == o;
035: @ ensures \result;
036: @ also
037: @ requires o == null;
038: @ diverges false;
039: @ ensures !\result;
040: @ also
041: @ requires o != null;
042: @ diverges false;
043: @ ensures \result == o.equals(this);
044: @*/
045: /** @preconditions true
046: * @postconditions result = (self=o)
047: * @modifies
048: */
049: public/*@ pure @*/boolean equals(Object o) {
050: }
051:
052: /** The Class of this object. Needed to specify that invoking
053: * getClass() on an object always produces the same result: no
054: * methods include this model field in their assignable clause,
055: * so no methods can alter the outcome of invoking getClass() on
056: * some object. This property is important when using ESC/Java
057: * on specs that use getClass(), just knowing that getClass() is
058: * pure is not enough.
059: */
060: //@ public model non_null Class _getClass;
061: //@ public represents _getClass <- \typeof(this);
062: // The value produced by hashCode() but without any side-effects.
063: /*@ public normal_behavior
064: @ ensures (\forall Object o; equals(o) ==> \result == o.hashValue());
065: @ public pure model int hashValue();
066: @*/
067:
068: /*@ public behavior
069: @ assignable objectState; // for subclasses with benevolent side effects
070: @ ensures \result == hashValue();
071: @ also
072: @ public normal_behavior
073: @ requires \typeof(this) == \type(Object);
074: @ assignable \nothing;
075: @*/
076: public int hashCode() {
077: }
078:
079: //@ public model String theString;
080:
081: /*@ public normal_behavior
082: @ assignable objectState;
083: @ ensures \result != null;
084: @ ensures \result == theString;
085: @ also
086: @ public normal_behavior
087: @ requires \typeof(this) == \type(Object);
088: @ assignable \nothing;
089: @ ensures \result != null;
090: @ implies_that
091: @ assignable objectState;
092: @ ensures \result != null;
093: @*/
094: public String toString() {
095: }
096:
097: /*@ protected behavior
098: @ requires objectTimesFinalized == 0 ; // FIXME && \lockset.isEmpty();
099: @ assignable objectTimesFinalized, objectState;
100: @ ensures objectTimesFinalized == 1;
101: @ signals (Throwable) objectTimesFinalized == 1;
102: @*/
103: protected void finalize() throws Throwable {
104: }
105:
106: protected Object clone() throws CloneNotSupportedException {
107: }
108:
109: /*@ public normal_behavior
110: @ ensures \result == _getClass;
111: @ ensures_redundantly \result != null;
112: @*/
113: public final native Class getClass();
114:
115: public final void notify() throws IllegalMonitorStateException {
116: }
117:
118: public final void notifyAll() throws IllegalMonitorStateException {
119: }
120:
121: public final void wait() throws IllegalMonitorStateException,
122: InterruptedException {
123: }
124:
125: //@ requires ms >= 0;
126: public final void wait(long ms)
127: throws IllegalMonitorStateException, InterruptedException {
128: }
129:
130: //@ requires ms >= 0 && 0 <= ns && ns < 1000000;
131: public final void wait(long ms, int ns)
132: throws IllegalMonitorStateException, InterruptedException {
133: }
134:
135: }
|