content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio.channels;
  
  public abstract class AsynchronousFileChannel extends java.lang.Object implements java.nio.channels.AsynchronousChannel
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected AsynchronousFileChannel();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.nio.channels.AsynchronousFileChannel open(java.nio.file.Path arg0, java.util.Set arg1, java.util.concurrent.ExecutorService arg2, java.nio.file.attribute.FileAttribute[] arg3) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.nio.channels.AsynchronousFileChannel open(java.nio.file.Path arg0, java.nio.file.OpenOption[] arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract long size() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.channels.AsynchronousFileChannel truncate(long arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void force(boolean arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract void lock(long arg0, long arg1, boolean arg2, java.lang.Object arg3, java.nio.channels.CompletionHandler arg4);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final void lock(java.lang.Object arg0, java.nio.channels.CompletionHandler arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.concurrent.Future lock(long arg0, long arg1, boolean arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.util.concurrent.Future lock();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.channels.FileLock tryLock(long arg0, long arg1, boolean arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final java.nio.channels.FileLock tryLock() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract void read(java.nio.ByteBuffer arg0, long arg1, java.lang.Object arg2, java.nio.channels.CompletionHandler arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.concurrent.Future read(java.nio.ByteBuffer arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract void write(java.nio.ByteBuffer arg0, long arg1, java.lang.Object arg2, java.nio.channels.CompletionHandler arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.util.concurrent.Future write(java.nio.ByteBuffer arg0, long arg1);
  }
  