FlexOr.io
Class BufferedInput

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

All Implemented Interfaces:

java.io.Closeable

public class BufferedInput
extends java.io.BufferedInputStream

BufferedInput extends the BufferedInputStream by providing the features for simple scanning of input.

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 structure for a file.

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

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

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

Class invariant: currentChar = input[i] => nextChar = input[i+1];

Version:

1.0 1999 Jan 10

Author:

Gunnar Gotshalks

Constructor Summary

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

Method Summary

int	getCharCount() Return the number of data characters read from the file.
int	getCurrentChar() The current character is the one to process next from the input file.
int	getLineCount()
int	getNextChar() The next character is a look ahead character.
int	read() Requires: True Ensures: currentChar = old nextChar nextChar = next character from the file or EOF if at the end of file.
java.lang.String	readLine() Requires: currentChar be the first character of the line to read.
void	skipToNextLine() Requires: True Ensures: forall c : old currentChar ..
void	skipWhitespaces() Requires: True Ensures: old currentChar ..

Methods inherited from class java.io.BufferedInputStream

available, close, mark, markSupported, read, reset, 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

BufferedInput

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

Creating an instance of BufferedInput opens the file named by the String. There is no open required by the user. In the OO paradigm opening a file is analogous to creating a new object unlike procedural paradigm where the same variables are reused for each file.

Requires: True
Ensures: currentChar = input[0]  // first char in the file

Throws:

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

Method Detail

getCurrentChar

public int getCurrentChar()

The current character is the one to process next from the input file.

Requires: user called read i times
Ensures: result = currentChar
     and currentChar = input[i-1]

getNextChar

public int getNextChar()

The next character is a look ahead character.

Requires: user called read i times
Ensures: result = nextChar
    and nextChar = input[i]

getCharCount

public int getCharCount()

Return the number of data characters read from the file.

Requires: True
Ensures:i : 0..N-1 | currentChar = input[i] => result = i+1
          and i: N, ... | currentChar = input[i] => result = N

getLineCount

public int getLineCount()

read

public int read()

Requires: True Ensures: currentChar = old nextChar nextChar = next character from the file or EOF if at the end of file. No need to test for EOF before reading as Java returns EOF an unbounded number of times. Need to have different cases depending upon how end-of-line is represented. On Macintosh it is '\r' (13), on Unix is is '\n' (10), on Windows it is '\r\n'. This means that after recognizing '\r' we must skip a following '\n'. End-of-line always counts as 1 character. EOF does not count as a character. ---------------------------

Overrides:

read in class java.io.BufferedInputStream

readLine

public java.lang.String readLine()

Requires: currentChar be the first character of the line to read. Ensures: result string contains the characters in the line up to the end-of-line. currentChar is the first character on the next line. ---------------------------

skipWhitespaces

public void skipWhitespaces()

Requires: True Ensures: old currentChar .. currentChar-1 are white space. currentChar is not a white space character (could be EOF) ---------------------------

skipToNextLine

public void skipToNextLine()

Requires: True Ensures: forall c : old currentChar .. currentChar-2 | c ~= EOL and c ~= EOF currentChar-1 = EOL => currentChar = first character on the next line or EOF currentChar-1 = EOF => currentChar = EOF ---------------------------