java.io
Class PrintStream

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

public class PrintStream

extends FilterOutputStream

JML's specification of PrintStream

Author:

David Cok, Gary T. Leavens, Patrice Chalin

Class Specifications

Specifications inherited from class FilterOutputStream

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
boolean	error

 

Model fields inherited from class java.io.FilterOutputStream

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
boolean	endsInNewLine
static String	eol
String	outputText

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary

 

Fields inherited from class java.io.FilterOutputStream

out

 

Constructor Summary

PrintStream(OutputStream os)

PrintStream(OutputStream os, boolean Param1)

PrintStream(OutputStream os, boolean Param1, String Param2)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
boolean	checkError()
void	close()
void	flush()
void	print(boolean Param0)
void	print(char Param0)
void	print(char[] Param0)
void	print(double Param0)
void	print(float Param0)
void	print(int Param0)
void	print(Object o)
void	print(String s)
void	print(long Param0)
void	println()
void	println(boolean b)
void	println(char Param0)
void	println(char[] Param0)
void	println(double Param0)
void	println(float Param0)
void	println(int i)
void	println(Object o)
void	println(String s)
void	println(long Param0)
protected  void	setError()
void	write(byte[] b, int off, int len)
void	write(int i)

 

Methods inherited from class java.io.FilterOutputStream

write

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

error

public boolean error

outputText

public String outputText

Specifications:
is in groups: outputBytes

endsInNewLine

public boolean endsInNewLine

Specifications:
is in groups: outputBytes

eol

public static final String eol

PrintStream

public PrintStream(OutputStream os)

Specifications:

ensures this.underlyingStream == os;

PrintStream

public PrintStream(OutputStream os,
                   boolean Param1)

Specifications:

ensures this.underlyingStream == os;

PrintStream

public PrintStream(OutputStream os,
                   boolean Param1,
                   String Param2)
            throws UnsupportedEncodingException

Throws:

UnsupportedEncodingException

Specifications:

ensures this.underlyingStream == os;

println

public void println()

Specifications:

public normal_behavior
assignable outputText, endsInNewLine;
ensures this.endsInNewLine;
ensures this.outputText.equals(\old(this.outputText)+java.io.PrintStream.eol);

setError

protected void setError()

Specifications:

protected normal_behavior
assignable error;
ensures this.error;

checkError

public boolean checkError()

Specifications:

public normal_behavior
requires !this.isOpen;
assignable error;
ensures this.error;
ensures \result == this.error;

print

public void print(char Param0)

println

public void println(char Param0)

println

public void println(String s)

Specifications:

public normal_behavior
assignable outputText, endsInNewLine;
ensures this.endsInNewLine;
ensures s != null ==> this.outputText.equals(\old(this.outputText)+s+java.io.PrintStream.eol);

print

public void print(String s)

Specifications:

public normal_behavior
assignable outputText, endsInNewLine;
ensures s != null ==> this.outputText.equals(\old(this.outputText)+s);

print

public void print(double Param0)

println

public void println(double Param0)

print

public void print(float Param0)

println

public void println(float Param0)

println

public void println(Object o)

Specifications:

requires true;
assignable outputText, endsInNewLine;
ensures this.endsInNewLine;
ensures this.outputText.startsWith(\old(this.outputText));

print

public void print(Object o)

Specifications:

requires true;
assignable outputText, endsInNewLine;
ensures this.outputText.startsWith(\old(this.outputText));

println

public void println(boolean b)

Specifications:

requires true;
assignable outputText, endsInNewLine;
ensures this.endsInNewLine;
ensures this.outputText.startsWith(\old(this.outputText));

print

public void print(boolean Param0)

print

public void print(int Param0)

println

public void println(int i)

Specifications:

requires true;
assignable outputText, endsInNewLine;
ensures this.endsInNewLine;
ensures this.outputText.startsWith(\old(this.outputText));

print

public void print(long Param0)

println

public void println(long Param0)

flush

public void flush()

Overrides:

flush in class FilterOutputStream

Specifications:

     also

public normal_behavior
requires !this.isOpen;
assignable error;
ensures this.error;

     also

public exceptional_behavior
assignable output, error;
signals (java.io.IOException) false;

Specifications inherited from overridden method in class FilterOutputStream:
      --- None ---

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 *);

print

public void print(char[] Param0)

println

public void println(char[] Param0)

write

public void write(int i)

Overrides:

write in class FilterOutputStream

Specifications inherited from overridden method in class FilterOutputStream:
      --- None ---

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[] b,
                  int off,
                  int len)

Overrides:

write in class FilterOutputStream

Specifications inherited from overridden method in class FilterOutputStream:
      --- None ---

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

close

public void close()

Overrides:

close in class FilterOutputStream

Specifications:

     also

public normal_behavior
requires !this.isOpen;
assignable error;
ensures this.error;

     also

public exceptional_behavior
assignable output, error;
signals (java.io.IOException) false;

Specifications inherited from overridden method in class FilterOutputStream:
      --- None ---

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 *);