Package components.simplewriter

Interface SimpleWriterKernel

All Superinterfaces:
AutoCloseable, Standard<SimpleWriter>
All Known Subinterfaces:
SimpleWriter
All Known Implementing Classes:
SimpleWriter1L, SimpleWriterSecondary
public interface SimpleWriterKernel extends Standard<SimpleWriter>, AutoCloseable
SimpleWriter 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 SimpleWriter is modeled by CHARACTER_STREAM_MODEL
Constructor(s) (initial abstract value(s) of this):
():
  ensures
    this = (true, <>, <>)
(String fileName):
  requires
    [fileName is the name of a file that exists and is writeable]
  ensures
    this = (true, fileName, <>)

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    close()
    Closes the stream.
    boolean
    isOpen()
    Reports whether the stream is open.
    String
    name()
    Reports the name of the stream.
    void
    write(char c)
    Appends <c> to the end of this.content without flushing the output buffer.

    Methods inherited from interface components.standard.Standard

    clear, newInstance, transferFrom

  • Method Details

    • write

      void write(char c)
      Appends <c> to the end of this.content without flushing the output buffer.
      Parameters:
      c - the character to output
      Updates:
      this.content
      Requires:
      this.is_open
      Ensures:
      this.content = #this.content * <c>

    • name

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

    • isOpen

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

    • close

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