FlexOr.io
Class CountedInput

java.lang.Object
  java.io.InputStream
      java.io.FilterInputStream
          java.io.BufferedInputStream
              FlexOr.io.CountedInput

All Implemented Interfaces:

java.io.Closeable

public class CountedInput
extends java.io.BufferedInputStream

CountedInput is meant to be used to process ASCII files. It provides a base for from which specific scanning files can be constructed. To help programmers provide some input statistics in application programs we provide charCount to count the total number of characters input from a file, charNumber to give the position of the character within the current line, and lineNumber of the current line. Scan and skip operations for whitespace and the rest of the current line are provided.

The Java file input API read method always returns a character, including an unbounded number of EOF characters when the end of file is reached. Consequently, all input files are implicitly unbounded in length giving the following logical structure for a file.

  file = input[0..N-1 , N, ...] 

where a file contains the N data characters input[0..N-1] and an unbounded number EOF characters in input[N, N+1, ...].

The EOL character (end-ofline) always counts as one data character. See the method read()

Definitions

charCount

The net number of characters read by the user taking backtracking (mark/reset) into account.

markCharCount

The net number of characters read by the user at the last mark. Value is 0 before the first call to mark.

#userReadCalls

The number of times the user has called read() since the last mark or reset.

lineNumber

One plus the net number of end-of-lines read by the user taking backtracking (mark/reset) into account.

#linesReadSinceMark

The number of EOLs read by the user since the last mark or reset.

position

The index of the next character to read. Initial value is 0.

Class invariant:

    charCount = max(markCharCount + #userReadCalls, #input)
    lineNumber = markLineNumber + #linesReadSinceMark
    0 <= position

Version:

1.0 1999 Jan 10

Author:

Gunnar Gotshalks

Constructor Summary

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

Method Summary

int	charCount() Return the net number of data characters read from the file.
int	charNumber() Return the position of the current character in the current line.
char	currentChar() Return the current character.
int	lineNumber() Return the current line number -- the net number of lines read from the file.
void	mark(int marklimit) Mark position for backtracking with reset.
int	read() Read the next character in the file.
java.lang.String	readLine() Reads the rest of the current line.
void	reset() Reset position to last mark point.
int	skipToNextLine() Skip to and return the first character on the next line.
int	skipWhitespace() Skip characters until a non whitespace character is read.
java.lang.String	spanNonWhitespace() Span non whitespace
java.lang.String	spanWhitespace() Span whitespace.

Methods inherited from class java.io.BufferedInputStream

available, close, markSupported, read, skip

Methods inherited from class java.io.FilterInputStream

read

Methods inherited from class java.lang.Object

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

Constructor Detail

CountedInput

public CountedInput(java.lang.String fileName)
             throws java.io.FileNotFoundException

Creating an instance of CountedInput opens the file named by the String. There is no open required by the user.

Requires:
    True
Ensures:
    charChar = 0 and lineNumber = 1 and position = 0 and
    charNumber = 0;

Throws:

java.io.FileNotFoundException - when the file named by fileName cannot be opened.

Method Detail

charCount

public int charCount()

Return the net number of data characters read from the file.

Requires:
    True

Returns:

charCount

charNumber

public int charNumber()

Return the position of the current character in the current line.

Requires:
    True

Returns:

charNumber

lineNumber

public int lineNumber()

Return the current line number -- the net number of lines read from the file.

Requires:
    True 

Returns:

lineNumber

currentChar

public char currentChar()

Return the current character.

Requires:
    True 

Returns:

currentChar

read

public int read()

Read the next character in the file.

Requires:
    True
Ensures:
    position = 1 + old position
    (  input[old position] = EOF and charCount = old charCount 
         and lineNumber = old lineNumber
     or
       input[old position] = EOL  and charCount = 1 + old charCount
         and charNumber = 0  and lineNumber = 1 + oldLineNumber
     or
       input[old position]  notin {EOL, EOF} and charCount = 1 + old charCount
         and charNumber = 1 + old charNumber  and lineNumber = old lineNumber
     )

Overrides:

read in class java.io.BufferedInputStream

Returns:

input[position-1]

readLine

public java.lang.String readLine()

Reads the rest of the current line. The next read will read the first character on the next line, if any, or read EOF. If the last read character was EOL or EOF then no characters are read -- rest of line is empty.

Requires:
    100 >= number of characters in rest of line
Ensures:
     input[old position .. position-2] intersect {EOF, EOL} = null
     input[position-1] in {EOF, EOL}

Returns:

input[old position .. position-2]

skipWhitespace

public int skipWhitespace()

Skip characters until a non whitespace character is read. EOF is not a whitespace character. Using whitespace definition in Character.isWhitespace

Requires:
    True
Ensures:
     input[old position .. position-1] intersect nonWhitespace = null

Returns:

input[position]

skipToNextLine

public int skipToNextLine()

Skip to and return the first character on the next line.

Requires:
    True
Ensures:
     input[old position .. position-1] intersect {EOL, EOF} = null

Returns:

input[position]

spanWhitespace

public java.lang.String spanWhitespace()

Span whitespace.

Requires:
    True
Ensures:
     input[old position .. position-1] intersect nonWhiteSpace = null

Returns:

input[old position .. position-1]

spanNonWhitespace

public java.lang.String spanNonWhitespace()

Span non whitespace

Requires:
    True
Ensures:
     input[old position .. position-1] intersect whiteSpace = null

Returns:

input[old position .. position-1]

mark

public void mark(int marklimit)

Mark position for backtracking with reset. Marklimit is the maximum read ahead before reset cannot be used.

Requires:
    True
Ensures:
    position = old position  and charNumber = old charNumber
    charCount = old charCount  and  lineNumber = old lineNumber
    markPosition = position  and markCharNumber = charNumber
    markCharCount = charCount  and  markLineNumber = lineNumber

Overrides:

mark in class java.io.BufferedInputStream

reset

public void reset()
           throws java.io.IOException

Reset position to last mark point.

Requires:
    mark(marklimit) toave been called
Ensures:
    markPosition = old markPosition
    markCharCount = old markCharCount
    markCharCount = old markCharCount
    markLineNumber = old markLineNumber
    markPosition = position
    markCharCount = charCount  and  markLineNumber = theLineNumber
    markCharNumber = charNumber

Overrides:

reset in class java.io.BufferedInputStream

Throws:

java.io.IOException - When position-markPosition > marklimit or mark(marklimit) has not been called.