// @(#)$Id: Method.jml,v 1.10 2008/10/15 01:11:27 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 Method extends AccessibleObject implements Member { //@ public model Class returnType; //@ public constraint returnType == \old(returnType); //@ ensures this.returnType == returnType; Method(Class declaringClass, String name, Class[] parameterTypes, Class returnType, Class[] checkedExceptions, int modifiers, int slot); Method 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 == returnType; @*/ public /*@ pure non_null @*/ Class getReturnType(); /*@ 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(); /*@ requires !Modifier.isStatic(getModifiers()) ==> obj != null; @ ensures getReturnType() == boolean.class ==> \result instanceof Boolean; @ ensures getReturnType() == byte.class ==> \result instanceof Byte; @ ensures getReturnType() == char.class ==> \result instanceof Character; @ ensures getReturnType() == int.class ==> \result instanceof Integer; @ ensures getReturnType() == long.class ==> \result instanceof Long; @ ensures getReturnType() == short.class ==> \result instanceof Short; @ ensures getReturnType() == double.class ==> \result instanceof Double; @ ensures getReturnType() == float.class ==> \result instanceof Float; @ ensures getReturnType() == void.class ==> \result == null; @ ensures_redundantly @ getReturnType().isPrimitive() && getReturnType() != void.class @ ==> \result != null; @*/ public /*@ nullable */ Object invoke(/*@nullable*/Object obj, Object[] args) throws IllegalAccessException, IllegalArgumentException, InvocationTargetException; // MethodAccessor is not a public class, it's a sun proprietary class // MethodAccessor getMethodAccessor(); // void setMethodAccessor(MethodAccessor accessor); static Class[] copy(Class[] in); }