Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

java.lang.reflect
Class Array

java.lang.Object
  extended byjava.lang.reflect.Array
public final class Array
extends Object

Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Constructor Summary
Array()
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
static Object get(Object Param0, int Param1)
           
static boolean getBoolean(Object Param0, int Param1)
           
static byte getByte(Object Param0, int Param1)
           
static char getChar(Object Param0, int Param1)
           
static double getDouble(Object Param0, int Param1)
           
static float getFloat(Object Param0, int Param1)
           
static int getInt(Object Param0, int Param1)
           
static int getLength(Object Param0)
           
static long getLong(Object Param0, int Param1)
           
static short getShort(Object Param0, int Param1)
           
static Object newInstance(Class Param0, int Param1)
           
static Object newInstance(Class Param0, int[] Param1)
           
static void set(Object Param0, int Param1, Object Param2)
           
static void setBoolean(Object Param0, int Param1, boolean Param2)
           
static void setByte(Object Param0, int Param1, byte Param2)
           
static void setChar(Object Param0, int Param1, char Param2)
           
static void setDouble(Object Param0, int Param1, double Param2)
           
static void setFloat(Object Param0, int Param1, float Param2)
           
static void setInt(Object Param0, int Param1, int Param2)
           
static void setLong(Object Param0, int Param1, long Param2)
           
static void setShort(Object Param0, int Param1, short Param2)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Array

public Array()
Method Detail

getLength

public static int getLength(Object Param0)
                     throws IllegalArgumentException
Throws:
IllegalArgumentException
Specifications: pure
requires \elemtype(\typeof(Param0)) <: \type(java.lang.Object);
ensures \result == ((java.lang.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;

getByte

public static byte getByte(Object Param0,
                           int Param1)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure
public behavior
requires true;
signals_only java.lang.ArrayIndexOutOfBoundsException, java.lang.IllegalArgumentException;
signals (java.lang.ArrayIndexOutOfBoundsException) Param1 < 0||getLength(Param0) <= Param1;
     also
public behavior
requires 0 <= Param1&&Param1 < getLength(Param0);
{|
requires \elemtype(\typeof(Param0)) <: \type(java.lang.Object);
ensures false;
also
requires \elemtype(\typeof(Param0)) == \type(int);
ensures false;
also
requires \elemtype(\typeof(Param0)) == \type(byte);
ensures \result == ((byte[])Param0)[Param1];
|}

getChar

public static char getChar(Object Param0,
                           int Param1)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

getDouble

public static double getDouble(Object Param0,
                               int Param1)
                        throws IllegalArgumentException,
                               ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

getFloat

public static float getFloat(Object Param0,
                             int Param1)
                      throws IllegalArgumentException,
                             ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

getInt

public static int getInt(Object Param0,
                         int Param1)
                  throws IllegalArgumentException,
                         ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure
public behavior
requires true;
signals_only java.lang.ArrayIndexOutOfBoundsException, java.lang.IllegalArgumentException;
signals (java.lang.ArrayIndexOutOfBoundsException) Param1 < 0||getLength(Param0) <= Param1;
     also
public behavior
requires 0 <= Param1&&Param1 < getLength(Param0);
{|
requires \elemtype(\typeof(Param0)) <: \type(java.lang.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];
|}

getLong

public static long getLong(Object Param0,
                           int Param1)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

getShort

public static short getShort(Object Param0,
                             int Param1)
                      throws IllegalArgumentException,
                             ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

getBoolean

public static boolean getBoolean(Object Param0,
                                 int Param1)
                          throws IllegalArgumentException,
                                 ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure

setByte

public static void setByte(Object Param0,
                           int Param1,
                           byte Param2)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setChar

public static void setChar(Object Param0,
                           int Param1,
                           char Param2)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setDouble

public static void setDouble(Object Param0,
                             int Param1,
                             double Param2)
                      throws IllegalArgumentException,
                             ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setFloat

public static void setFloat(Object Param0,
                            int Param1,
                            float Param2)
                     throws IllegalArgumentException,
                            ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setInt

public static void setInt(Object Param0,
                          int Param1,
                          int Param2)
                   throws IllegalArgumentException,
                          ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setLong

public static void setLong(Object Param0,
                           int Param1,
                           long Param2)
                    throws IllegalArgumentException,
                           ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setShort

public static void setShort(Object Param0,
                            int Param1,
                            short Param2)
                     throws IllegalArgumentException,
                            ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

setBoolean

public static void setBoolean(Object Param0,
                              int Param1,
                              boolean Param2)
                       throws IllegalArgumentException,
                              ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException

newInstance

public static Object newInstance(Class Param0,
                                 int Param1)
                          throws NegativeArraySizeException
Throws:
NegativeArraySizeException
Specifications: pure

newInstance

public static Object newInstance(Class Param0,
                                 int[] Param1)
                          throws IllegalArgumentException,
                                 NegativeArraySizeException
Throws:
IllegalArgumentException
NegativeArraySizeException
Specifications: pure

get

public static Object get(Object Param0,
                         int Param1)
                  throws IllegalArgumentException,
                         ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Specifications: pure nullable
public behavior
requires true;
signals_only java.lang.ArrayIndexOutOfBoundsException, java.lang.IllegalArgumentException;
signals (java.lang.ArrayIndexOutOfBoundsException) Param1 < 0||getLength(Param0) <= Param1;
     also
public behavior
requires 0 <= Param1&&Param1 < getLength(Param0);
{|
requires \elemtype(\typeof(Param0)) <: \type(java.lang.Object);
ensures \result == ((java.lang.Object[])Param0)[Param1];
also
requires \elemtype(\typeof(Param0)) == \type(int);
ensures \result != null;
ensures \result instanceof java.lang.Integer;
ensures ((java.lang.Integer)\result ).intValue() == ((int[])Param0)[Param1];
also
requires \elemtype(\typeof(Param0)) == \type(byte);
ensures \result != null;
ensures \result instanceof java.lang.Byte;
ensures ((java.lang.Byte)\result ).byteValue() == ((byte[])Param0)[Param1];
|}

set

public static void set(Object Param0,
                       int Param1,
                       Object Param2)
                throws IllegalArgumentException,
                       ArrayIndexOutOfBoundsException
Throws:
IllegalArgumentException
ArrayIndexOutOfBoundsException
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.