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 FileChannel extends java.nio.channels.spi.AbstractInterruptibleChannel implements java.nio.channels.SeekableByteChannel, java.nio.channels.GatheringByteChannel, java.nio.channels.ScatteringByteChannel
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected FileChannel();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.nio.channels.FileChannel open(java.nio.file.Path arg0, java.util.Set arg1, java.nio.file.attribute.FileAttribute[] arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public static java.nio.channels.FileChannel 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 int read(java.nio.ByteBuffer arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract long read(java.nio.ByteBuffer[] arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final long read(java.nio.ByteBuffer[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract int write(java.nio.ByteBuffer arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract long write(java.nio.ByteBuffer[] arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final long write(java.nio.ByteBuffer[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract long position() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.channels.FileChannel position(long arg0) 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.FileChannel 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; signals (java.io.IOException e) true; */
     public abstract long transferTo(long arg0, long arg1, java.nio.channels.WritableByteChannel arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract long transferFrom(java.nio.channels.ReadableByteChannel arg0, long arg1, long arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract int read(java.nio.ByteBuffer arg0, long arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract int write(java.nio.ByteBuffer arg0, long arg1) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.MappedByteBuffer map(java.nio.channels.FileChannel$MapMode arg0, long arg1, long arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract java.nio.channels.FileLock lock(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 lock() throws java.io.IOException;
  
     /*@ 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; signals (java.io.IOException e) true; */
     public java.nio.channels.SeekableByteChannel truncate(long arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.nio.channels.SeekableByteChannel position(long arg0) throws java.io.IOException;
  }
  