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 interface SeekableByteChannel extends java.nio.channels.ByteChannel
  {
  
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int read(java.nio.ByteBuffer arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int write(java.nio.ByteBuffer arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public long position() 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;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public long size() 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;
  }
  