content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.io;
  
  public abstract class Writer extends java.lang.Object implements java.lang.Appendable, java.io.Closeable, java.io.Flushable
  {
     protected java.lang.Object lock;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected Writer();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected Writer(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void write(int arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void write(char[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void write(char[] arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void write(java.lang.String arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void write(java.lang.String arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.io.Writer append(java.lang.CharSequence arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.io.Writer 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.io.Writer append(char arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void flush() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract void close() throws java.io.IOException;
  
     /*@ 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;
  }
  