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 abstract class FileSystem extends java.lang.Object implements java.io.Closeable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected FileSystem();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.file.spi.FileSystemProvider provider();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void close() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isOpen();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isReadOnly();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.lang.String getSeparator();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.lang.Iterable getRootDirectories();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.lang.Iterable getFileStores();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.Set supportedFileAttributeViews();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.file.Path getPath(java.lang.String arg0, java.lang.String[] arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.file.PathMatcher getPathMatcher(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.file.attribute.UserPrincipalLookupService getUserPrincipalLookupService();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.file.WatchService newWatchService() throws java.io.IOException;
  }
  