content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.lang;
  
  public final class Class extends java.lang.Object implements java.io.Serializable, java.lang.reflect.GenericDeclaration, java.lang.reflect.Type, java.lang.reflect.AnnotatedElement
  {
     java.lang.ClassValue$ClassValueMap classValueMap;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.ClassNotFoundException e) true; */
     public static java.lang.Class forName(java.lang.String arg0) throws java.lang.ClassNotFoundException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.ClassNotFoundException e) true; */
     public static java.lang.Class forName(java.lang.String arg0, boolean arg1, java.lang.ClassLoader arg2) throws java.lang.ClassNotFoundException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.InstantiationException e) true; signals (java.lang.IllegalAccessException e) true; */
     public java.lang.Object newInstance() throws java.lang.InstantiationException, java.lang.IllegalAccessException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isInstance(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAssignableFrom(java.lang.Class arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isInterface();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isArray();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isPrimitive();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAnnotation();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSynthetic();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.ClassLoader getClassLoader();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.TypeVariable[] getTypeParameters();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class getSuperclass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Type getGenericSuperclass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Package getPackage();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class[] getInterfaces();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Type[] getGenericInterfaces();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class getComponentType();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getModifiers();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object[] getSigners();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Method getEnclosingMethod();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.reflect.Constructor getEnclosingConstructor();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class getDeclaringClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class getEnclosingClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getSimpleName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getCanonicalName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAnonymousClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isLocalClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMemberClass();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class[] getClasses();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Field[] getFields() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Method[] getMethods() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Constructor[] getConstructors() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchFieldException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Field getField(java.lang.String arg0) throws java.lang.NoSuchFieldException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchMethodException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Method getMethod(java.lang.String arg0, java.lang.Class[] arg1) throws java.lang.NoSuchMethodException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchMethodException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Constructor getConstructor(java.lang.Class[] arg0) throws java.lang.NoSuchMethodException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.Class[] getDeclaredClasses() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Field[] getDeclaredFields() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Method[] getDeclaredMethods() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Constructor[] getDeclaredConstructors() throws java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchFieldException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Field getDeclaredField(java.lang.String arg0) throws java.lang.NoSuchFieldException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchMethodException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Method getDeclaredMethod(java.lang.String arg0, java.lang.Class[] arg1) throws java.lang.NoSuchMethodException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NoSuchMethodException e) true; signals (java.lang.SecurityException e) true; */
     public java.lang.reflect.Constructor getDeclaredConstructor(java.lang.Class[] arg0) throws java.lang.NoSuchMethodException, java.lang.SecurityException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.InputStream getResourceAsStream(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.net.URL getResource(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.security.ProtectionDomain getProtectionDomain();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean desiredAssertionStatus();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isEnum();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object[] getEnumConstants();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object cast(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Class asSubclass(java.lang.Class arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation getAnnotation(java.lang.Class arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAnnotationPresent(java.lang.Class arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation[] getAnnotations();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.annotation.Annotation[] getDeclaredAnnotations();
  }
  