001package components.simplewriter;
002
003import components.standard.Standard;
004
005/**
006 * SimpleWriter 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 SimpleWriter is modeled by CHARACTER_STREAM_MODEL
021 * @initially {@code
022 * ():
023 *   ensures
024 *     this = (true, <>, <>)
025 * (String fileName):
026 *   requires
027 *     [fileName is the name of a file that exists and is writeable]
028 *   ensures
029 *     this = (true, fileName, <>)
030 * }
031 */
032public interface SimpleWriterKernel extends Standard<SimpleWriter>, AutoCloseable {
033
034    /**
035     * Appends {@code <c>} to the end of {@code this.content} without flushing
036     * the output buffer.
037     *
038     * @param c
039     *            the character to output
040     * @updates this.content
041     * @requires this.is_open
042     * @ensures {@code this.content = #this.content * <c>}
043     */
044    void write(char c);
045
046    /**
047     * Reports the name of the stream.
048     *
049     * @return {@code this.ext_name}
050     * @ensures name = this.ext_name
051     */
052    String name();
053
054    /**
055     * Reports whether the stream is open.
056     *
057     * @return true iff {@code this} is open
058     * @ensures isOpen = this.is_open
059     */
060    boolean isOpen();
061
062    /**
063     * Closes the stream.
064     *
065     * @updates this
066     * @requires this.is_open
067     * @ensures {@code this = (false, <>, <>)}
068     */
069    @Override
070    void close();
071
072}