java.lang
Class Throwable

java.lang.Object
  java.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

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

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

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;