java.io
Class InputStream

java.lang.Object
  java.io.InputStream

Direct Known Subclasses:

ObjectInputStream, ServletInputStream

public abstract class InputStream

extends Object

JML's specification of InputStream.

Author:

David Cok (following Leaven's spec of OutputStream)

Class Specifications

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
boolean	_markSupported
int	availableBytes
JMLDataGroup	input           The input data group is used to specify things like caching, and to make sure that methods that might produce some internal side effects have a side effect on some datagroup.
JMLValueSequence	inputBytes
boolean	isOpen
\bigint	markLimit
\bigint	markPosition
\bigint	readPosition
boolean	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

InputStream()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
int	available()
void	close()
void	mark(int readLimit)
boolean	markSupported()
abstract  int	read()
int	read(byte[] b)
int	read(byte[] b, int off, int len)
void	reset()
long	skip(long n)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

input

public JMLDataGroup input

The input data group is used to specify things like caching, and to make sure that methods that might produce some internal side effects have a side effect on some datagroup.

Specifications:
is in groups: objectState
datagroup contains: inputBytes readPosition availableBytes isOpen wasClosed

inputBytes

public JMLValueSequence inputBytes

Specifications: non_null
is in groups: input

readPosition

public \bigint readPosition

Specifications:
is in groups: input

availableBytes

public int availableBytes

Specifications:
is in groups: input

isOpen

public boolean isOpen

Specifications:
is in groups: input

wasClosed

public boolean wasClosed

Specifications:
is in groups: input

_markSupported

public boolean _markSupported

Specifications:
is in groups: objectState

markPosition

public \bigint markPosition

Specifications:
is in groups: objectState

markLimit

public \bigint markLimit

Specifications:
is in groups: objectState

InputStream

public InputStream()

Specifications:

public normal_behavior
assignable isOpen, wasClosed;
ensures this.isOpen&&!this.wasClosed;

close

public void close()
           throws IOException

Throws:

IOException

Specifications:

public behavior
assignable isOpen, wasClosed;
ensures !this.isOpen&&this.wasClosed;
signals_only java.io.IOException;
signals (java.io.IOException) (* an IO error occured *);

read

public abstract int read()
                  throws IOException

Throws:

IOException

Specifications:

public normal_behavior
requires this.isOpen&&(this.inputBytes.length() == this.readPosition);
assignable \nothing;
ensures \result == -1;

     also

requires this.isOpen&&(this.inputBytes.length() > this.readPosition);
assignable readPosition, objectState, availableBytes;
ensures this.isOpen;
ensures \result == \old(((org.jmlspecs.models.JMLByte)this.inputBytes.itemAt(this.readPosition)).theByte);
ensures this.readPosition == \old(this.readPosition+1);
ensures 0 <= \result &&\result <= 255;

     also

public exceptional_behavior
requires !this.isOpen;
assignable \nothing;
signals_only java.io.IOException;

read

public int read(byte[] b)
         throws IOException

Throws:

IOException

Specifications:

public normal_behavior
requires this.isOpen&&(this.inputBytes.length() == this.readPosition);
assignable \nothing;
ensures \result == -1;

     also

public behavior
old \bigint arraylen = b.length;
old \bigint data = this.inputBytes.length()-this.readPosition;
requires this.isOpen&&(this.inputBytes.length() > this.readPosition);
assignable inputBytes, objectState, availableBytes, b[*];
ensures this.isOpen;
ensures \result >= 0;
ensures \result <= arraylen;
ensures \result <= data;
ensures arraylen > 0 ==> \result > 0;
ensures arraylen >= this.availableBytes&&data >= this.availableBytes ==> \result >= this.availableBytes;
ensures this.readPosition == \old(this.readPosition)+\result ;
ensures ( \forall int i; 0 <= i&&i < \result ; b[i] == \old(((org.jmlspecs.models.JMLByte)this.inputBytes.itemAt(i+this.readPosition)).theByte));
ensures ( \forall int i; \result <= i&&i < b.length; b[i] == \old(b[i]));

     also

public exceptional_behavior
requires !this.isOpen;
assignable \nothing;
signals_only java.io.IOException;

read

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

Throws:

IOException

Specifications:

public normal_behavior
requires this.isOpen&&(this.inputBytes.length() == this.readPosition);
assignable \nothing;
ensures \result == -1;

     also

old \bigint data = this.inputBytes.length()-this.readPosition;
requires this.isOpen&&(this.inputBytes.length() > this.readPosition);
assignable readPosition, objectState, availableBytes, b[off .. off+len-1];
ensures this.isOpen;
ensures \result >= 0;
ensures \result <= len;
ensures \result <= data;
ensures len > 0 ==> \result > 0;
ensures len >= this.availableBytes&&data >= this.availableBytes ==> \result >= this.availableBytes;
ensures this.readPosition == \old(this.readPosition)+\result ;
ensures ( \forall int i; 0 <= i&&i < \result ; b[off+i] == \old(((org.jmlspecs.models.JMLByte)this.inputBytes.itemAt(i+this.readPosition)).theByte));
ensures ( \forall int i; (0 <= i&&i < off)||(off+\result <= i&&i < b.length); b[i] == \old(b[i]));

     also

public exceptional_behavior
requires !this.isOpen;
assignable \nothing;
signals_only java.io.IOException;

skip

public long skip(long n)
          throws IOException

Throws:

IOException

Specifications:

public normal_behavior
requires this.isOpen&&(this.inputBytes.length() == this.readPosition);
assignable \nothing;
ensures \result == 0;

     also

public normal_behavior
requires this.isOpen&&n < 0;
assignable \nothing;
ensures \result == 0;

     also

old \bigint data = this.inputBytes.length()-this.readPosition;
requires this.isOpen&&(this.inputBytes.length() > this.readPosition);
assignable readPosition, availableBytes;
ensures this.isOpen;
ensures \result >= 0;
ensures \result <= n;
ensures \result <= data;
ensures n >= this.availableBytes&&data >= this.availableBytes ==> \result >= this.availableBytes;
ensures this.readPosition == \old(this.readPosition)+\result ;

     also

public exceptional_behavior
requires !this.isOpen;
assignable \nothing;
signals_only java.io.IOException;

available

public int available()
              throws IOException

Throws:

IOException

Specifications: pure

public normal_behavior
requires this.isOpen;
ensures \result == this.availableBytes;

mark

public void mark(int readLimit)

Specifications:

public normal_behavior
requires this._markSupported;
assignable markPosition, markLimit, objectState;
ensures this.markPosition == this.readPosition;
ensures this.markLimit == this.readPosition+readLimit;

markSupported

public boolean markSupported()

Specifications: pure

public normal_behavior
ensures \result == this._markSupported;

reset

public void reset()
           throws IOException

Throws:

IOException

Specifications:

public normal_behavior
requires this._markSupported&&this.markLimit >= this.readPosition&&this.markPosition != -1;
assignable readPosition;
ensures this.markPosition == this.readPosition;

     also

public behavior
requires this._markSupported&&this.markPosition == -1;
assignable readPosition;
ensures 0 == this.readPosition;

     also

public exceptional_behavior
assignable \nothing;
signals_only java.io.IOException;
signals (java.io.IOException e) this.markPosition == -1||this.readPosition > this.markLimit;