FlexOr.io
Class CountedOutput

java.lang.Object
  java.io.OutputStream
      java.io.FilterOutputStream
          java.io.BufferedOutputStream
              FlexOr.io.CountedOutput

All Implemented Interfaces:

java.io.Closeable, java.io.Flushable

public class CountedOutput
extends java.io.BufferedOutputStream

CountedOutput extends the BufferedOutputStream by providing the features for counting characters and lines of output, and methods to output specific structures.

Version:

1.0 1999 Jan 10

Author:

Gunnar Gotshalks

Constructor Summary

CountedOutput(java.lang.String fileName)
Creating an instance of CountedOutput opens the named file.

Method Summary

int	charCount() Return the number of data characters written to the file.
int	getTabstopDist() Return the tabstop distance.
int	lineCount() Return the number of lines written to the file.
int	lineLength() Return the number of characters written to the current line.
void	setTabstopDist(int newTabstop) Set the tabstop distance.
void	write(byte[] buffer, int offset, int count) Output a buffer of characters.
void	write(int theChar) Output a single character
void	write(java.lang.String string) Output a string.
void	writeInteger(int integer) Output an integer in the minimum space.
void	writeInteger(int integer, int width) Requires: length(stringRep(integer)) <= width Ensures: output = output^spaces^stringRep(integer) #spaces = width - length(stringRep(integer)) charCount = width + old CharCount
void	writeln(java.lang.String string) Output a string of characters followed by a newline.
void	writeNewline() Output a newline character
void	writeNoCount(byte[] buffer, int offset, int count) Output a buffer without adding to the lineLength.
void	writeNoCount(java.lang.String string) Output a string without adding to the lineLength.

Methods inherited from class java.io.BufferedOutputStream

flush

Methods inherited from class java.io.FilterOutputStream

close, write

Methods inherited from class java.lang.Object

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

Constructor Detail

CountedOutput

public CountedOutput(java.lang.String fileName)
              throws java.io.IOException

Creating an instance of CountedOutput opens the named file.

Requires:
    True
Ensures:
    charChar = 0 and lineCount = 0

Throws:

java.io.IOException - When the output file cannot be created.

Method Detail

charCount

public int charCount()

Return the number of data characters written to the file.

Requires:
    True

Returns:

charCount

lineCount

public int lineCount()

Return the number of lines written to the file.

Requires:
    True 

Returns:

lineCount

lineLength

public int lineLength()

Return the number of characters written to the current line.

Requires:
    True 

Returns:

lineCount

getTabstopDist

public int getTabstopDist()

Return the tabstop distance.

Requires:
    True 

Returns:

tabstopDist

setTabstopDist

public void setTabstopDist(int newTabstop)

Set the tabstop distance.

Requires:
    True
Ensures:
    tabstopDist = newTabstop

write

public void write(int theChar)

Output a single character

Requires: True Ensures: output = output^theChar charCount = 1 + oldCharCount

Overrides:

write in class java.io.BufferedOutputStream

writeNewline

public void writeNewline()

Output a newline character

Requires: True Ensures: output = output^Character.EOL theCharCount = 1 + old CharCount and lineCount = 1 + old lineCount

write

public void write(java.lang.String string)

Output a string.

Requires: True Ensures: output = output^string charCount = string.length + old CharCount lineCount = old lineCount + #(newLines in string)

writeln

public void writeln(java.lang.String string)

Output a string of characters followed by a newline.

Requires: True Ensures: output = output^string^Character.EOL theCharCount = length(string) + 1 + old CharCount lineCount = 1 + old lineCount

writeNoCount

public void writeNoCount(java.lang.String string)

Output a string without adding to the lineLength. Often used when markup tags are output as they do not add to the effective line length. The total number of output characters is incremented.

Requires: True Ensures: output = output^string charCount = string.length() + old CharCount lineCount = old lineCount

write

public void write(byte[] buffer,
                  int offset,
                  int count)

Output a buffer of characters.

Requires: True Ensures: output = output^buffer[offset .. offset+count-1] charCount = count + old CharCount lineCount = old lineCount + #(newLines in buffer[offset .. offset+count-1])

Overrides:

write in class java.io.BufferedOutputStream

writeNoCount

public void writeNoCount(byte[] buffer,
                         int offset,
                         int count)

Output a buffer without adding to the lineLength. Often used when markup tags are output as they do not add to the effective line length. The total number of output characters is incremented.

Requires: True Ensures: output = output^buffer[offset .. offset+count-1] charCount = count + old CharCount lineCount = old lineCount

writeInteger

public void writeInteger(int integer)

Output an integer in the minimum space.

Requires: True Ensures: output = output^stringRep(integer) theCharCount = length(stringRep(integer)) + old CharCount

writeInteger

public void writeInteger(int integer,
                         int width)

Requires: length(stringRep(integer)) <= width Ensures: output = output^spaces^stringRep(integer) #spaces = width - length(stringRep(integer)) charCount = width + old CharCount