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 class Package extends java.lang.Object implements java.lang.reflect.AnnotatedElement
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getSpecificationTitle();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getSpecificationVersion();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getSpecificationVendor();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getImplementationTitle();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getImplementationVersion();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getImplementationVendor();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSealed();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSealed(java.net.URL arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.lang.NumberFormatException e) true; */
     public boolean isCompatibleWith(java.lang.String arg0) throws java.lang.NumberFormatException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.Package getPackage(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.lang.Package[] getPackages();
  
     /*@ 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.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();
  }
  