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 interface BasicFileAttributes
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.attribute.FileTime lastModifiedTime();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.attribute.FileTime lastAccessTime();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.attribute.FileTime creationTime();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isRegularFile();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isDirectory();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSymbolicLink();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isOther();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long size();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object fileKey();
  }
  