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 class PrintStream extends java.io.FilterOutputStream implements java.lang.Appendable, java.io.Closeable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public PrintStream(java.io.OutputStream arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public PrintStream(java.io.OutputStream arg0, boolean arg1);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.UnsupportedEncodingException e) true; */
     public PrintStream(java.io.OutputStream arg0, boolean arg1, java.lang.String arg2) throws java.io.UnsupportedEncodingException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.FileNotFoundException e) true; */
     public PrintStream(java.lang.String arg0) throws java.io.FileNotFoundException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.FileNotFoundException e) true; signals (java.io.UnsupportedEncodingException e) true; */
     public PrintStream(java.lang.String arg0, java.lang.String arg1) throws java.io.FileNotFoundException, java.io.UnsupportedEncodingException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.FileNotFoundException e) true; */
     public PrintStream(java.io.File arg0) throws java.io.FileNotFoundException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.FileNotFoundException e) true; signals (java.io.UnsupportedEncodingException e) true; */
     public PrintStream(java.io.File arg0, java.lang.String arg1) throws java.io.FileNotFoundException, java.io.UnsupportedEncodingException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public void flush();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void close();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean checkError();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void setError();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void clearError();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void write(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void write(byte[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void print(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println();
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(boolean arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(char[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public void println(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream printf(java.lang.String arg0, java.lang.Object[] arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream printf(java.util.Locale arg0, java.lang.String arg1, java.lang.Object[] arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream format(java.lang.String arg0, java.lang.Object[] arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream format(java.util.Locale arg0, java.lang.String arg1, java.lang.Object[] arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream append(java.lang.CharSequence arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream append(java.lang.CharSequence arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.io.PrintStream append(char 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;
  }
  