JML

java.lang
Class Throwable

java.lang.Object
  extended byjava.lang.Throwable
All Implemented Interfaces:
Serializable
Direct Known Subclasses:
Error, Exception, UnpositionedError

public class Throwable
extends Object
implements Serializable


Class Specifications
public invariant \nonnullelements(this._stackTrace);
public represents causeSet <- this._cause != this;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 Throwable _cause
           
 String _message
           
 StackTraceElement[] _stackTrace
           
 boolean causeSet
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Constructor Summary
Throwable()
           
Throwable(non_null String message)
           
Throwable(non_null String message, nullable Throwable cause)
           
Throwable(nullable Throwable cause)
           
 
Model Method Summary
 boolean initMessage(nullable Throwable c)
           
 boolean standardThrowable()
           
 boolean standardThrowable(non_null String s)
           
 boolean standardThrowable(non_null String s, nullable Throwable c)
           
 boolean standardThrowable(nullable Throwable c)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Throwable fillInStackTrace()
           
 Throwable getCause()
           
 String getLocalizedMessage()
           
 String getMessage()
           
 StackTraceElement[] getStackTrace()
           
 Throwable initCause(non_null Throwable cause)
           
 void printStackTrace()
           
 void printStackTrace(non_null PrintStream s)
           
 void printStackTrace(non_null PrintWriter s)
           
 void setStackTrace(non_null StackTraceElement[] stackTrace)
           
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Model Field Detail

_message

public String _message
Specifications: nullable
is in groups: objectState

_cause

public Throwable _cause
Specifications: nullable
is in groups: objectState
datagroup contains: causeSet

causeSet

public boolean causeSet
Specifications:
is in groups: _cause

_stackTrace

public StackTraceElement[] _stackTrace
Specifications: non_null
is in groups: objectState
Constructor Detail

Throwable

public Throwable()
Specifications: pure
public normal_behavior
assignable _message, _cause, _stackTrace;
ensures this._message == null;
ensures !this.causeSet;
ensures_redundantly this.standardThrowable();

Throwable

public Throwable(non_null String message)
Specifications: pure
public normal_behavior
assignable _message, _cause, _stackTrace;
ensures this._message == message;
ensures !this.causeSet;
ensures_redundantly this.standardThrowable(message);

Throwable

public Throwable(non_null String message,
                 nullable Throwable cause)
Specifications: pure
public normal_behavior
requires cause != this;
assignable _message, _cause, _stackTrace;
ensures this._message == message;
ensures this._cause == cause;
ensures_redundantly this.standardThrowable(message,cause);

Throwable

public Throwable(nullable Throwable cause)
Specifications: pure
public normal_behavior
requires cause != this;
assignable _message, _cause, _stackTrace;
ensures this.initMessage(cause);
ensures this._cause == cause;
ensures_redundantly this.standardThrowable(cause);
Model Method Detail

standardThrowable

public boolean standardThrowable()
Specifications: pure
public normal_behavior
ensures \result == (this._message == null&&!this.causeSet);

standardThrowable

public boolean standardThrowable(non_null String s)
Specifications: pure
public normal_behavior
ensures \result == (this._message == s&&!this.causeSet);

standardThrowable

public boolean standardThrowable(nullable Throwable c)
Specifications: pure
public normal_behavior
requires c != this;
ensures \result == (this.initMessage(c)&&this._cause == c);
ensures_redundantly this.causeSet;

standardThrowable

public boolean standardThrowable(non_null String s,
                                 nullable Throwable c)
Specifications: pure
public normal_behavior
requires c != this;
ensures \result == (this._message == s&&this._cause == c);
ensures_redundantly this.causeSet;

initMessage

public boolean initMessage(nullable Throwable c)
Specifications: pure
public normal_behavior
requires c != null;
ensures \result == (this._message != null&&this._message.equals(c.toString()));
     also
public normal_behavior
requires c == null;
ensures \result == (this._message == null);
Method Detail

getMessage

public String getMessage()
Specifications: pure nullable
public normal_behavior
ensures \result == this._message;

getLocalizedMessage

public String getLocalizedMessage()
Specifications: pure nullable
public normal_behavior
requires this._message == null;
ensures \result == null;
     also
public normal_behavior
requires this._message != null;
ensures \result != null;
ensures (* \result is a localized version of _message *);

getCause

public Throwable getCause()
Specifications: pure nullable
public normal_behavior
requires this.causeSet;
ensures \result == this._cause;
     also
public normal_behavior
requires !this.causeSet;
ensures \result == null;

initCause

public Throwable initCause(non_null Throwable cause)
Specifications: non_null
public normal_behavior
requires !this.causeSet&&cause != this;
assignable _cause;
ensures this.causeSet;
     also
public exceptional_behavior
requires this.causeSet||cause == this;
assignable \nothing;
signals_only java.lang.IllegalStateException, java.lang.IllegalArgumentException;
signals (java.lang.IllegalStateException e) this.causeSet&&e._message != null&&!e.causeSet;
signals (java.lang.IllegalArgumentException e) cause == this&&e._message != null&&!e.causeSet;

toString

public String toString()
Overrides:
toString in class Object
Specifications: pure non_null
     also
public normal_behavior
requires \typeof(this) == \type(java.lang.Throwable);
ensures this._message == null ==> \result .equals(this.getClass().theString);
ensures this._message != null ==> \result .equals(this.getClass().theString+": "+this._message);
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;

printStackTrace

public void printStackTrace()

printStackTrace

public void printStackTrace(non_null PrintStream s)

printStackTrace

public void printStackTrace(non_null PrintWriter s)

fillInStackTrace

public Throwable fillInStackTrace()
Specifications: non_null
public normal_behavior
assignable _stackTrace;
ensures \result == this;

getStackTrace

public StackTraceElement[] getStackTrace()
Specifications: pure non_null
public normal_behavior
ensures \result != null;
ensures ( \forall int i; 0 <= i&&i < this._stackTrace.length; this._stackTrace[i].equals(\result [i]));

setStackTrace

public void setStackTrace(non_null StackTraceElement[] stackTrace)
Specifications:
public normal_behavior
requires \nonnullelements(stackTrace);
assignable _stackTrace;
ensures this._stackTrace.equals(stackTrace);
     also
public exceptional_behavior
requires !\nonnullelements(stackTrace);
assignable \nothing;
signals_only java.lang.NullPointerException;

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.