java.io
Class OutputStream

java.lang.Object
  java.io.OutputStream

Direct Known Subclasses:

ByteArrayOutputStream, FilterOutputStream, ServletOutputStream

public abstract class OutputStream

extends Object

JML's specification of OutputStream.

Author:

Gary T. Leavens

Class Specifications

public invariant ( \forall int i; 0 <= i&&i < this.outputBytes.size(); this.outputBytes.get(i) instanceof org.jmlspecs.models.JMLByte); public invariant this.isOpen ==> !this.wasClosed; public invariant this.wasClosed ==> !this.isOpen; public constraint \old(this.wasClosed) ==> this.wasClosed;

Specifications inherited from class Object

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

Model Field Summary
boolean	isOpen           Is this file open?
JMLDataGroup	output           The output data group is used to specify things like caching, and to make sure that methods that might produce some output have a side effect on some datagroup.
JMLValueSequence	outputBytes           The bytes that are to be (or have been) output.
boolean	wasClosed           Was this file closed?

 

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

OutputStream()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	close()
void	flush()
void	write(byte[] b)
void	write(byte[] b, int off, int len)
abstract  void	write(int i)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

output

public JMLDataGroup output

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

Specifications:
is in groups: objectState
datagroup contains: outputBytes

outputBytes

public JMLValueSequence outputBytes

The bytes that are to be (or have been) output.

Specifications: non_null
is in groups: output
datagroup contains: java.io.PrintStream.outputText java.io.PrintStream.endsInNewLine

isOpen

public boolean isOpen

Is this file open?

Specifications:
is in groups: objectState

wasClosed

public boolean wasClosed

Was this file closed?

Specifications:
is in groups: objectState

OutputStream

public OutputStream()

Specifications:

public normal_behavior
assignable isOpen, outputBytes;
ensures this.outputBytes.isEmpty()&&!this.isOpen&&!this.wasClosed;

close

public void close()
           throws IOException

Throws:

IOException

Specifications:

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

flush

public void flush()
           throws IOException

Throws:

IOException

Specifications:

public behavior
requires this.isOpen;
assignable output;
ensures (* the output is written to the device *);
signals_only java.io.IOException;
signals (java.io.IOException) (* an IO error occured *);

write

public abstract void write(int i)
                    throws IOException

Throws:

IOException

Specifications:

public behavior
requires this.isOpen;
assignable outputBytes;
ensures this.outputBytes.equals(\old(this.outputBytes.insertBack(new org.jmlspecs.models.JMLByte((byte)i))));
signals_only java.io.IOException;
signals (java.io.IOException) (* an IO error occured *);

write

public void write(byte[] b)
           throws IOException

Throws:

IOException

Specifications:

public behavior
old \bigint siz = this.outputBytes.size();
requires this.isOpen;
assignable outputBytes;
ensures this.outputBytes.size() == siz+b.length&&( \forall int i; 0 <= i&&i < siz; this.outputBytes.get(i).equals(\old(this.outputBytes.get(i))))&&( \forall int k; 0 <= k&&k < b.length; this.outputBytes.get(siz+k).equals(new org.jmlspecs.models.JMLByte(b[k])));
signals_only java.io.IOException, java.lang.NullPointerException;
signals (java.io.IOException) b != null&&(* an IO error occured *);
signals (java.lang.NullPointerException) b == null;

write

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

Throws:

IOException

Specifications:

public behavior
old \bigint siz = this.outputBytes.size();
requires this.isOpen&&b != null&&off >= 0&&len >= 0&&off+len <= b.length;
assignable outputBytes;
ensures this.outputBytes.size() == siz+len&&( \forall int i; 0 <= i&&i < siz; this.outputBytes.get(i).equals(\old(this.outputBytes.get(i))))&&( \forall int k; off <= k&&k < off+len; this.outputBytes.get(siz+k).equals(new org.jmlspecs.models.JMLByte(b[off+k])));
signals_only java.io.IOException;
signals (java.io.IOException) (* an IO error occured *);

     also

public exceptional_behavior
requires this.isOpen&&(b == null||off < 0||len < 0||off+len > b.length);
assignable \nothing;
signals_only java.io.IOException, java.lang.IndexOutOfBoundsException, java.lang.NullPointerException;
signals (java.lang.IndexOutOfBoundsException) off < 0||len < 0||off+len > b.length;
signals (java.lang.NullPointerException) b == null;

     also

public model_program { ... }