content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.lang.reflect;
  
  public final class Constructor extends java.lang.reflect.AccessibleObject implements java.lang.reflect.GenericDeclaration, java.lang.reflect.Member
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class getDeclaringClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getModifiers();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.TypeVariable[] getTypeParameters();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class[] getParameterTypes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Type[] getGenericParameterTypes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class[] getExceptionTypes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Type[] getGenericExceptionTypes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toGenericString();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InstantiationException e) true; signals (java.lang.IllegalAccessException e) true; signals (java.lang.IllegalArgumentException e) true; signals (java.lang.reflect.InvocationTargetException e) true; */
     public java.lang.Object newInstance(java.lang.Object[] arg0) throws java.lang.InstantiationException, java.lang.IllegalAccessException, java.lang.IllegalArgumentException, java.lang.reflect.InvocationTargetException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isVarArgs();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSynthetic();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation getAnnotation(java.lang.Class arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation[] getDeclaredAnnotations();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation[][] getParameterAnnotations();
  }
  