Package components.simplereader

Interface SimpleReaderKernel

All Superinterfaces:
AutoCloseable, Standard<SimpleReader>
All Known Subinterfaces:
SimpleReader
All Known Implementing Classes:
SimpleReader1L, SimpleReaderSecondary
public interface SimpleReaderKernel extends Standard<SimpleReader>, AutoCloseable
SimpleReader kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Subtypes:
CHARACTER_STREAM_MODEL is (
  is_open: boolean,
  ext_name: string of character,
  content: string of character)
 exemplar cs
 constraint
  if not cs.is_open
    then (cs.ext_name = <> and
          cs.content = <>)
Mathematical Model (abstract value and abstract invariant of this):
type SimpleReader is modeled by CHARACTER_STREAM_MODEL
Constructor(s) (initial abstract value(s) of this):
():
  ensures
    this = (true, <>, [contents of stdin])
(String name):
  requires
    [name is the name of a file that exists and is readable or
     name is a valid URL that is accessible]
  ensures
    this = (true, name,
     [contents of the file or of the page referred to by the name])

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    atEOS()
    Reports whether the end of the stream has been reached.
    void
    close()
    Closes the stream.
    boolean
    isOpen()
    Reports whether the stream is open.
    String
    name()
    Reports the name of the stream.
    char
    peek()
    Peeks a single char from this.content.
    char
    read()
    Reads a single char from this.content.

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom

  • Method Details

    • read

      char read()
      Reads a single char from this.content.
      Returns:
      the char read
      Updates:
      this.content
      Requires:
      this.is_open and this.content /= <>
      Ensures:
      #this.content = <read> * this.content

    • peek

      char peek()
      Peeks a single char from this.content.
      Returns:
      the char peeked
      Requires:
      this.is_open and this.content /= <>
      Ensures:
      <peek> is prefix of this.content

    • isOpen

      boolean isOpen()
      Reports whether the stream is open.
      Returns:
      true iff this is open
      Ensures:
      isOpen = this.is_open

    • name

      String name()
      Reports the name of the stream.
      Returns:
      this.ext_name
      Ensures:
      name = this.ext_name

    • atEOS

      boolean atEOS()
      Reports whether the end of the stream has been reached.
      Returns:
      true iff this is at end-of-stream
      Requires:
      this.is_open
      Ensures:
      atEOS = (this.content = <>)

    • close

      void close()
      Closes the stream.
      Specified by:
      close in interface AutoCloseable
      Updates:
      this
      Requires:
      this.is_open
      Ensures:
      this = (false, <>, <>)