// @(#)$Id: Array.refines-spec,v 1.4 2006/08/08 17:18:50 perryjames Exp $

// Copyright (C) 2005 Iowa State University
//
// This file is part of the runtime library of the Java Modeling Language.
//
// This library is free software; you can redistribute it and/or
// modify it under the terms of the GNU Lesser General Public License
// as published by the Free Software Foundation; either version 2.1,
// of the License, or (at your option) any later version.
//
// This library 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
// Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with JML; see the file LesserGPL.txt.  If not, write to the Free
// Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
// 02110-1301  USA.

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_only ArrayIndexOutOfBoundsException,
      @                IllegalArgumentException;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @ 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_only ArrayIndexOutOfBoundsException,
      @                IllegalArgumentException;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @ 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_only ArrayIndexOutOfBoundsException,
      @                IllegalArgumentException;
      @   signals (ArrayIndexOutOfBoundsException) Param1 < 0 || getLength(Param0) <= Param1;
      @ 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 /*@nullable*/ 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;
}