// @(#)$Id: Constructor.jml,v 1.10 2005/12/23 17:02:03 chalin 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 Constructor extends AccessibleObject implements Member { Constructor(Class declaringClass, Class[] parameterTypes, Class[] checkedExceptions, int modifiers, int slot); Constructor copy(); /*@ also public normal_behavior @ ensures \result != null; @*/ public /*@ pure @*/ Class getDeclaringClass(); /*@ also public normal_behavior @ ensures \result != null; @*/ public /*@ pure @*/ String getName(); public /*@ pure @*/ int getModifiers(); /*@ public normal_behavior @ ensures \result != null; @*/ public /*@ pure @*/ Class[] getParameterTypes(); /*@ public normal_behavior @ ensures \result != null; @*/ public /*@ pure @*/ Class[] getExceptionTypes(); public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object obj); public /*@ pure @*/ int hashCode(); public /*@ pure non_null @*/ String toString(); public /*@ non_null @*/ Object newInstance(Object[] initargs) throws InstantiationException, IllegalAccessException, IllegalArgumentException, InvocationTargetException; // ConstructorAccessor is a sun proprietary class // ConstructorAccessor getConstructorAccessor(); // void setConstructorAccessor(ConstructorAccessor accessor); int getSlot(); }