content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio.file.attribute;
  
  public final class FileTime extends java.lang.Object implements java.lang.Comparable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.file.attribute.FileTime from(long arg0, java.util.concurrent.TimeUnit arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.file.attribute.FileTime fromMillis(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long to(java.util.concurrent.TimeUnit arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public long toMillis();
  
     /*@ 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 int compareTo(java.nio.file.attribute.FileTime arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  