content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio;
  
  public abstract class CharBuffer extends java.nio.Buffer implements java.lang.Comparable, java.lang.Appendable, java.lang.CharSequence, java.lang.Readable
  {
     final char[] hb;
     final int offset;
     boolean isReadOnly;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.CharBuffer allocate(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.CharBuffer wrap(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.CharBuffer wrap(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int read(java.nio.CharBuffer arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.CharBuffer wrap(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.CharBuffer wrap(java.lang.CharSequence arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer slice();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer duplicate();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer asReadOnlyBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract char get();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer put(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract char get(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer put(int arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer get(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer get(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer put(java.nio.CharBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer put(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.CharBuffer put(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer put(java.lang.String arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.CharBuffer put(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean hasArray();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final char[] array();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int arrayOffset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer compact();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isDirect();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.nio.CharBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int length();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final char charAt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer subSequence(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer append(java.lang.CharSequence arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer append(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.CharBuffer append(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteOrder order();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object array();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.lang.Appendable append(char arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.lang.Appendable append(java.lang.CharSequence arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.lang.Appendable append(java.lang.CharSequence arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.CharSequence subSequence(int arg0, int arg1);
  }
  