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;
  
  public interface Path extends java.lang.Comparable, java.lang.Iterable, java.nio.file.Watchable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.FileSystem getFileSystem();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAbsolute();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path getRoot();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path getFileName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path getParent();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getNameCount();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path getName(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path subpath(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean startsWith(java.nio.file.Path arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean startsWith(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean endsWith(java.nio.file.Path arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean endsWith(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path normalize();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path resolve(java.nio.file.Path arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path resolve(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path resolveSibling(java.nio.file.Path arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path resolveSibling(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path relativize(java.nio.file.Path arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.net.URI toUri();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.file.Path toAbsolutePath();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.nio.file.Path toRealPath(java.nio.file.LinkOption[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.File toFile();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.nio.file.WatchKey register(java.nio.file.WatchService arg0, java.nio.file.WatchEvent$Kind[] arg1, java.nio.file.WatchEvent$Modifier[] arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.nio.file.WatchKey register(java.nio.file.WatchService arg0, java.nio.file.WatchEvent$Kind[] arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.util.Iterator iterator();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.nio.file.Path 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();
  }
  