javax.servlet
Class ServletInputStream

java.lang.Object
  java.io.InputStream
      javax.servlet.ServletInputStream

public abstract class ServletInputStream

extends InputStream

JML's specification of ServletInputStream

Class Specifications

Specifications inherited from class InputStream

public invariant ( \forall int i; 0 <= i&&i < this.inputBytes.size(); this.inputBytes.get(i) instanceof org.jmlspecs.models.JMLByte); public invariant this.readPosition >= 0&&this.readPosition <= this.inputBytes.length(); public invariant this.availableBytes >= 0; public invariant this.isOpen ==> !this.wasClosed; public invariant this.wasClosed ==> !this.isOpen; public constraint this.inputBytes == \old(this.inputBytes); public initially this.readPosition == 0; initially this.markPosition == -1;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.io.InputStream

_markSupported, availableBytes, input, inputBytes, isOpen, markLimit, markPosition, readPosition, wasClosed

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary
protected	ServletInputStream()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
int	readLine(byte[] b, int off, int len)

 

Methods inherited from class java.io.InputStream

available, close, mark, markSupported, read, read, read, reset, skip

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

ServletInputStream

protected ServletInputStream()

readLine

public int readLine(byte[] b,
                    int off,
                    int len)
             throws IOException

Throws:

IOException