content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.lang;
  
  abstract class AbstractStringBuilder extends java.lang.Object implements java.lang.Appendable, java.lang.CharSequence
  {
     char[] value;
     int count;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public int length();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int capacity();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void ensureCapacity(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void trimToSize();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setLength(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public char charAt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int codePointAt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int codePointBefore(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int codePointCount(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int offsetByCodePoints(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void getChars(int arg0, int arg1, char[] arg2, int arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void setCharAt(int arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(java.lang.StringBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(java.lang.CharSequence arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(char[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder append(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder delete(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder appendCodePoint(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder deleteCharAt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder replace(int arg0, int arg1, java.lang.String arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String substring(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.CharSequence subSequence(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String substring(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, char[] arg1, int arg2, int arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, java.lang.Object arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, java.lang.String arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, char[] arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, java.lang.CharSequence arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, java.lang.CharSequence arg1, int arg2, int arg3);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, boolean arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, float arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder insert(int arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int indexOf(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int indexOf(java.lang.String arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int lastIndexOf(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int lastIndexOf(java.lang.String arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.AbstractStringBuilder reverse();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.lang.String toString();
  
     /*@ 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;
  }
  