// $Id: Throwable.jml 2226 2006-12-13 01:57:30Z chalin $

// Copyright (C) 2004 David Cok, Joe Kiniry

// This file is part of JML

// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.

// JML is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.

// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING.  If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.

/*
 * @author David Cok <cok@frontiernet.net>
 * @author Joe Kiniry <kiniry@cs.kun.nl>
 *
 * @todo kiniry - Replace use of java.lang.String with JMLString?
 *
 */

package java.lang;
// @ model import java.util.Arrays;

public class Throwable extends Object
    implements java.io.Serializable
{

    //@ public model String _message;  in objectState;
    //+@ public represents _message <- getMessage();
    
    //@ public model Throwable _cause; in objectState;
    //+@ public represents _cause <- getCause();

    //@ public model boolean causeKnown;  in objectState;

    // Note: cause is known if it was set in a constructor, even if it was
    // set to null

    //@ public model StackTraceElement[] _stackTrace; in objectState;
    //@ public represents _stackTrace <- getStackTrace();

    // public invariant (_stackTrace != null) ==> \nonnullelements(_stackTrace);

    /*@
      @ public normal_behavior
      @   ensures \result <==> (_message == s && !causeKnown && _cause == null
                     && theString.equals(getClass().theString + 
                                      (_message != null ? ": " + _message 
                                      : "")));
      @
        public pure model boolean standardThrowable(String s);

      @ public normal_behavior
      @   ensures \result <==> 
      @                ((s != null ==> _message == s)
      @              && ((s==null && c == null) ==> _message==null)
      @              && ((s==null && c != null) ==> (_message != null
                              && _message.equals(c.getClass().theString)))
      @              && causeKnown && _cause == c
                     && theString.equals(getClass().theString + 
                                      (_message != null ? ": " + _message 
                                      : "")));
      @
        public pure model boolean standardThrowable(String s, Throwable c);
      @*/

    /*@ public normal_behavior
      @   assignable this.*;
      @   ensures standardThrowable(null);
      @*/
    public /*@ pure @*/ Throwable();

    /*@ public normal_behavior
      @   assignable this.*;
      @   ensures standardThrowable(message);
      @*/
    public /*@ pure @*/ Throwable(String message);

    /*@ public normal_behavior
      @   ensures standardThrowable(message,cause);
      @*/
    public /*@ pure @*/ Throwable(String message, Throwable cause);

    /*@ public normal_behavior
      @   ensures standardThrowable(null,cause);
      @*/
    public /*@ pure @*/ Throwable(Throwable cause);

    /*@ public normal_behavior
      @   ensures \result == _message;
      @*/
    public /*@ pure @*/ String getMessage();

    // FIXME - I think the docs say this returns getMessage() unless
    // overridden; there is no automatic translation to a "localized" version
    // Even what is stated here is not right.
    /*@ public normal_behavior
      @   ensures (getMessage() != null) <==> (\result != null);
      @*/
    public /*@ pure @*/ String getLocalizedMessage();

    /*@ public normal_behavior
      @   ensures \result == _cause;
      @*/
    public /*@ pure @*/ Throwable getCause();

    /*@ public normal_behavior
      @   requires !causeKnown && cause != this;
      @   assignable _cause, causeKnown, theString, theHashCode;
      @   ensures \not_modified(_message);
      @   ensures getCause() == cause;
      @   ensures \result == this;
      @   ensures causeKnown;
          ensures theString.equals(getClass().theString + 
                                      (_message != null ? ": " + _message 
                                      : ""));
      @ also
      @ public exceptional_behavior
      @   requires causeKnown;
      @   assignable \nothing;
      @   signals_only IllegalStateException;
      @   signals (IllegalStateException e) e._message != null && !e.causeKnown;
      @ also
      @ public exceptional_behavior
      @   requires !causeKnown && cause == this;
      @   assignable \nothing;
      @   signals_only IllegalArgumentException;
      @   signals (IllegalArgumentException e) e._message != null && !e.causeKnown;
      @*/
    public synchronized Throwable initCause(Throwable cause);

    /*@ 
      @ also public normal_behavior
      @   requires \typeof(this) == \type(Throwable);
      @   ensures _message == null ==> \result.equals(this.getClass().theString);
      @   ensures _message != null ==> \result.equals(this.getClass().theString + ": " + _message);
      @ 
      @*/
    public /*@ pure @*/ String toString();

    // FIXME - need to indicate that the output streams are modified and not
    // other stuff
    // Prints to System.err
    public void printStackTrace();

    /*@ public normal_behavior
      @   assignable \not_specified;
      @*/
    public void printStackTrace(/*@non_null*/ java.io.PrintStream s);

    /*@ public normal_behavior
      @   assignable \not_specified;
      @*/
    public void printStackTrace(/*@non_null*/ java.io.PrintWriter s);

    /*@ public normal_behavior
      @   assignable _stackTrace;
      @   ensures \result == this;
      @*/
    public synchronized native /*@non_null*/ Throwable fillInStackTrace();

    /*+@ public normal_behavior  // FIXME - this crashes Simplify
      @   ensures (\forall int i; 0 <= i && i < _stackTrace.length;
      @                           _stackTrace[i].equals(\result[i]));
      @*/
    public /*@ pure @*//*@non_null*/ StackTraceElement[] getStackTrace();

    /*@ public normal_behavior
      @   requires stackTrace != null;
      @   requires \nonnullelements(stackTrace);
      @   assignable _stackTrace;
      @   ensures _stackTrace.equals (stackTrace);
      @ also
      @ public exceptional_behavior
      @   requires stackTrace == null;
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @ also
      @ public exceptional_behavior
      @   requires !\nonnullelements(stackTrace);
      @   assignable \nothing;
      @   signals_only NullPointerException;
      @*/
    public void setStackTrace(StackTraceElement[] stackTrace);
}
