// Generated by jmlspec from the .class file

package java.lang;

public class StringIndexOutOfBoundsException extends IndexOutOfBoundsException {

    /*@ public normal_behavior
      @   ensures standardThrowable(null);
      @*/
    //@ pure
    public StringIndexOutOfBoundsException();

    /*@ public normal_behavior
      @  ensures _cause == null && !causeKnown;
      @  ensures _message != null; // FIXME - more info using the index
      @*/
    //@ pure
    public StringIndexOutOfBoundsException(int index);

    /*@ public normal_behavior
      @   ensures standardThrowable(message);
      @*/
    //@ pure
    public StringIndexOutOfBoundsException(java.lang.String message);
}
