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 FileLock extends java.lang.Object implements java.lang.AutoCloseable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected FileLock(java.nio.channels.FileChannel arg0, long arg1, long arg2, boolean arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected FileLock(java.nio.channels.AsynchronousFileChannel arg0, long arg1, long arg2, boolean arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.channels.FileChannel channel();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.channels.Channel acquiredBy();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final long position();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final long size();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean isShared();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean overlaps(long arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isValid();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void release() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final void close() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String toString();
  }
  