content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.io;
  
  public class File extends java.lang.Object implements java.io.Serializable, java.lang.Comparable
  {
     public final static char separatorChar;
     public final static java.lang.String separator;
     public final static char pathSeparatorChar;
     public final static java.lang.String pathSeparator;
     final static boolean $assertionsDisabled;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public File(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public File(java.lang.String arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public File(java.io.File arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public File(java.net.URI arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getParent();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File getParentFile();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getPath();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAbsolute();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getAbsolutePath();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File getAbsoluteFile();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.lang.String getCanonicalPath() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.io.File getCanonicalFile() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public java.net.URL toURL() throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.net.URI toURI();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean canRead();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean canWrite();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean exists();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isDirectory();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isFile();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isHidden();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long lastModified();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long length();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public boolean createNewFile() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean delete();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void deleteOnExit();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String[] list();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String[] list(java.io.FilenameFilter arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File[] listFiles();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File[] listFiles(java.io.FilenameFilter arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File[] listFiles(java.io.FileFilter arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean mkdir();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean mkdirs();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean renameTo(java.io.File arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setLastModified(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setReadOnly();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setWritable(boolean arg0, boolean arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setWritable(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setReadable(boolean arg0, boolean arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setReadable(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setExecutable(boolean arg0, boolean arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean setExecutable(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean canExecute();
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.io.File[] listRoots();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long getTotalSpace();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long getFreeSpace();
  
     /*@ requires true; ensures true; assignable \everything; */
     public long getUsableSpace();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.io.File createTempFile(java.lang.String arg0, java.lang.String arg1, java.io.File arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.io.File createTempFile(java.lang.String arg0, java.lang.String arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.io.File arg0);
  
     /*@ 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 java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path toPath();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  