content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.util;
  
  public class Date extends java.lang.Object implements java.io.Serializable, java.lang.Cloneable, java.lang.Comparable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date();
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date(int arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date(int arg0, int arg1, int arg2, int arg3, int arg4);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date(int arg0, int arg1, int arg2, int arg3, int arg4, int arg5);
  
     /*@ requires true; ensures true; assignable \everything; */
     public Date(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object clone();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long UTC(int arg0, int arg1, int arg2, int arg3, int arg4, int arg5);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static long parse(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getYear();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setYear(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getMonth();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setMonth(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getDate();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setDate(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getDay();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getHours();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setHours(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getMinutes();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setMinutes(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getSeconds();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setSeconds(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long getTime();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setTime(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean before(java.util.Date arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean after(java.util.Date arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.util.Date 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 toLocaleString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toGMTString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getTimezoneOffset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  