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 InputStream extends java.lang.Object implements java.io.Closeable
  {
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public InputStream();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public abstract int read() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int read(byte[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int read(byte[] arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public long skip(long arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public int available() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void close() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public void mark(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public void reset() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean markSupported();
  }
  