001package components.simplereader;
002
003import components.standard.Standard;
004
005/**
006 * SimpleReader kernel component with primary methods. (Note: by package-wide
007 * convention, all references are non-null.)
008 *
009 * @mathsubtypes {@code
010 * CHARACTER_STREAM_MODEL is (
011 *   is_open: boolean,
012 *   ext_name: string of character,
013 *   content: string of character)
014 *  exemplar cs
015 *  constraint
016 *   if not cs.is_open
017 *     then (cs.ext_name = <> and
018 *           cs.content = <>)
019 * }
020 * @mathmodel type SimpleReader is modeled by CHARACTER_STREAM_MODEL
021 * @initially {@code
022 * ():
023 *   ensures
024 *     this = (true, <>, [contents of stdin])
025 * (String source):
026 *   requires
027 *     [source is the name of a file that exists and is readable or
028 *      source is a valid URL that is accessible]
029 *   ensures
030 *     this = (true, source,
031 *      [contents of the file or of the page referred to by the source])
032 * }
033 */
034public interface SimpleReaderKernel extends Standard<SimpleReader>, AutoCloseable {
035
036    /**
037     * Reads a single {@code char} from {@code this.content}.
038     *
039     * @return the {@code char} read
040     * @updates this.content
041     * @requires {@code this.is_open and this.content /= <>}
042     * @ensures {@code #this.content = <read> * this.content}
043     */
044    char read();
045
046    /**
047     * Peeks a single {@code char} from {@code this.content}.
048     *
049     * @return the {@code char} peeked
050     * @requires {@code this.is_open and this.content /= <>}
051     * @ensures {@code <peek> is prefix of this.content}
052     */
053    char peek();
054
055    /**
056     * Reports whether the stream is open.
057     *
058     * @return true iff {@code this} is open
059     * @ensures isOpen = this.is_open
060     */
061    boolean isOpen();
062
063    /**
064     * Reports the name of the stream.
065     *
066     * @return {@code this.ext_name}
067     * @ensures name = this.ext_name
068     */
069    String name();
070
071    /**
072     * Reports whether the end of the stream has been reached.
073     *
074     * @return true iff {@code this} is at end-of-stream
075     * @ensures {@code atEOS = (this.content = <>)}
076     */
077    boolean atEOS();
078
079    /**
080     * Closes the stream.
081     *
082     * @updates this
083     * @requires this.is_open
084     * @ensures {@code this = (false, <>, <>)}
085     */
086    @Override
087    void close();
088
089}