// Generated by jmlspec from the .class file

// FIXME
package java.lang.reflect;

public final class Array extends java.lang.Object {


    /*@
      @   requires \elemtype(\typeof(Param0)) <: \type(Object);
      @   ensures \result == ((Object[])Param0).length;
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(int);
      @   ensures \result == ((int[])Param0).length;
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(byte);
      @   ensures \result == ((byte[])Param0).length;
	// FIXME - do the rest of the primitive types
	// Also if not an array then throw an exception - FIXME

      @*/
    //@ pure
    public static native int getLength(java.lang.Object Param0)
        throws java.lang.IllegalArgumentException;

    /*@
      @ public behavior
      @   requires true;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @   signals (IllegalArgumentException) true;
      @   signals (Exception e) e instanceof ArrayIndexOutOfBoundsException ||
				e instanceof IllegalArgumentException;
      @ also public behavior
      @ requires 0 <= Param1 && Param1 < getLength(Param0);
      @ {|
      @   requires \elemtype(\typeof(Param0)) <: \type(Object);
      @   ensures false;
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(int);
      @   ensures false;
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(byte);
      @   ensures \result == ((byte[])Param0)[Param1];
      @ |}
	// FIXME - do the rest of the primitive types
	// Also if not an array then throw an exception - FIXME

      @ 
      @*/
    //@ pure
    public static native byte getByte(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native char getChar(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native double getDouble(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native float getFloat(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ public behavior
      @   requires true;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @   signals (IllegalArgumentException) true;
      @   signals (Exception e) e instanceof ArrayIndexOutOfBoundsException ||
				e instanceof IllegalArgumentException;
      @ also public behavior
      @ requires 0 <= Param1 && Param1 < getLength(Param0);
      @ {|
      @   requires \elemtype(\typeof(Param0)) <: \type(Object);
      @   ensures false;
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(int);
      @   ensures \result == ((int[])Param0)[Param1];
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(byte);
      @   ensures \result == ((byte[])Param0)[Param1];
      @ |}
	// FIXME - do the rest of the primitive types
	// Also if not an array then throw an exception - FIXME

      @ 
      @*/
    //@ pure
    public static native int getInt(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native long getLong(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native short getShort(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static native boolean getBoolean(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setByte(java.lang.Object Param0, int Param1, byte Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setChar(java.lang.Object Param0, int Param1, char Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setDouble(java.lang.Object Param0, int Param1, double Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setFloat(java.lang.Object Param0, int Param1, float Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setInt(java.lang.Object Param0, int Param1, int Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setLong(java.lang.Object Param0, int Param1, long Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setShort(java.lang.Object Param0, int Param1, short Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void setBoolean(java.lang.Object Param0, int Param1, boolean Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    //@ pure
    public static java.lang.Object newInstance(java.lang.Class Param0, int Param1)
        throws java.lang.NegativeArraySizeException;

    /*@
      @ 
      @*/
    //@ pure
    public static java.lang.Object newInstance(java.lang.Class Param0, int[] Param1)
        throws java.lang.IllegalArgumentException, java.lang.NegativeArraySizeException;

    /*@
      @ public behavior
      @   requires true;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @   signals (IllegalArgumentException) true;
      @   signals (Exception e) e instanceof ArrayIndexOutOfBoundsException ||
				e instanceof IllegalArgumentException;
      @ also public behavior
      @ requires 0 <= Param1 && Param1 < getLength(Param0);
      @ {|
      @   requires \elemtype(\typeof(Param0)) <: \type(Object);
      @   ensures \result == ((Object[])Param0)[Param1];
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(int);
      @   ensures \result != null;
      @   ensures \result instanceof Integer;
      @   ensures ((Integer)\result).intValue() == ((int[])Param0)[Param1];
      @ also
      @   requires \elemtype(\typeof(Param0)) == \type(byte);
      @   ensures \result != null;
      @   ensures \result instanceof Byte;
      @   ensures ((Byte)\result).byteValue() == ((byte[])Param0)[Param1];
      @ |}
	// FIXME - do the rest of the primitive types
	// Also if not an array then throw an exception - FIXME

      @ 
      @*/
    //@ pure
    public static native java.lang.Object get(java.lang.Object Param0, int Param1)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;

    /*@
      @ 
      @*/
    public static native void set(java.lang.Object Param0, int Param1, java.lang.Object Param2)
        throws java.lang.IllegalArgumentException, java.lang.ArrayIndexOutOfBoundsException;
}
