java.io
Class FilterOutputStream

java.lang.Object
  java.io.OutputStream
      java.io.FilterOutputStream

Direct Known Subclasses:

PrintStream

public class FilterOutputStream

extends OutputStream

Class Specifications

protected represents underlyingStream <- this.out;

Specifications inherited from class OutputStream

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
OutputStream	underlyingStream

 

Model fields inherited from class java.io.OutputStream

isOpen, output, outputBytes, 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

 

Field Summary
protected  OutputStream	out

 

Constructor Summary

FilterOutputStream(OutputStream out)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	close()
void	flush()
void	write(byte[] Param0)
void	write(byte[] Param0, int Param1, int Param2)
void	write(int Param0)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

underlyingStream

public OutputStream underlyingStream

out

protected OutputStream out

Specifications: non_null

FilterOutputStream

public FilterOutputStream(OutputStream out)

Specifications:

ensures this.underlyingStream == out;

close

public void close()
           throws IOException

Overrides:

close in class OutputStream

Throws:

IOException

Specifications inherited from overridden method in class OutputStream:

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

Overrides:

flush in class OutputStream

Throws:

IOException

Specifications inherited from overridden method in class OutputStream:

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 void write(int Param0)
           throws IOException

Throws:

IOException

Specifications inherited from overridden method write(int i) in class OutputStream:

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[] Param0)
           throws IOException

Overrides:

write in class OutputStream

Throws:

IOException

Specifications inherited from overridden method write(byte[] b) in class OutputStream:

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[] Param0,
                  int Param1,
                  int Param2)
           throws IOException

Overrides:

write in class OutputStream

Throws:

IOException

Specifications inherited from overridden method write(byte[] b, int off, int len) in class OutputStream:

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 { ... }