// Generated by jmlspec from the .class file

package java.lang;

public class IndexOutOfBoundsException extends java.lang.RuntimeException {

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

    /*@ public normal_behavior
      @   ensures standardThrowable(s);
      @*/
    //@ pure
    public IndexOutOfBoundsException(String s);
}
