001package components.simplereader;
002
003/**
004 * {@code SimpleReaderKernel} enhanced with secondary methods.
005 *
006 * @mathdefinitions <pre>
007 * LINE_SEPARATOR: string of character is
008 *   [character(s) used to denote line separator on the system where the input stream
009 *    content was created]
010 * </pre>
011 */
012public interface SimpleReader extends SimpleReaderKernel {
013
014    /**
015     * Reads a line from {@code this.content}, up to and including the first
016     * line separator (or the end of the stream), and returns everything up to
017     * the line separator (if any).
018     *
019     * @return the line read without the line separator
020     * @updates this.content
021     * @requires {@code this.is_open and this.content /= <>}
022     * @ensures {@code
023     * if LINE_SEPARATOR is substring of #this.content
024     *   then (#this.content = nextLine * LINE_SEPARATOR * this.content)
025     *   else (nextLine = #this.content  and  this.content = <>)
026     * }
027     */
028    String nextLine();
029
030    /**
031     * Reads a line from {@code this.content}, up to and including the first
032     * line separator (or the end of the stream), where the string before the
033     * line separator is the string representation of an {@code int}, and
034     * returns that {@code int}.
035     *
036     * @return the {@code int} read
037     * @updates this.content
038     * @requires {@code
039     * this.is_open  and
040     * there exists i: integer
041     *   (Integer.MIN_VALUE <= i  and  i <= Integer.MAX_VALUE  and
042     *    (TO_STRING(i) * LINE_SEPARATOR is prefix of this.content  or
043     *     TO_STRING(i) = this.content))
044     * }
045     * @ensures {@code
046     * if LINE_SEPARATOR is substring of #this.content
047     *   then (#this.content = TO_STRING(nextInteger) * LINE_SEPARATOR * this.content)
048     *   else (TO_STRING(nextInteger) = #this.content  and  this.content = <>)
049     * }
050     */
051    int nextInteger();
052
053    /**
054     * Reads a line from {@code this.content}, up to and including the first
055     * line separator (or the end of the stream), where the string before the
056     * line separator is the string representation of a {@code long}, and
057     * returns that {@code long}.
058     *
059     * @return the {@code long} read
060     * @updates this.content
061     * @requires {@code
062     * this.is_open  and
063     * there exists i: integer
064     *   (Long.MIN_VALUE <= i  and  i <= Long.MAX_VALUE  and
065     *    (TO_STRING(i) * LINE_SEPARATOR is prefix of this.content  or
066     *     TO_STRING(i) = this.content))
067     * }
068     * @ensures {@code
069     * if LINE_SEPARATOR is substring of #this.content
070     *   then (#this.content = TO_STRING(nextLong) * LINE_SEPARATOR * this.content)
071     *   else (TO_STRING(nextLong) = #this.content  and  this.content = <>)
072     * }
073     */
074    long nextLong();
075
076    /**
077     * Reads a line from {@code this.content}, up to and including the first
078     * line separator (or the end of the stream), where the string before the
079     * line separator is the string representation of a {@code boolean}, and
080     * returns that {@code boolean}.
081     *
082     * @return the {@code boolean} read
083     * @updates this.content
084     * @requires <pre>
085     * this.is_open  and
086     * there exists b: boolean
087     *   (TO_STRING(b) * LINE_SEPARATOR is prefix of this.content  or
088     *    TO_STRING(b) = this.content))
089     * </pre>
090     * @ensures {@code
091     * if LINE_SEPARATOR is substring of #this.content
092     *   then (#this.content = TO_STRING(nextBoolean) * LINE_SEPARATOR * this.content)
093     *   else (TO_STRING(nextBoolean) = #this.content  and  this.content = <>)
094     * }
095     */
096    boolean nextBoolean();
097
098    /**
099     * Reads a line from {@code this.content}, up to and including the first
100     * line separator (or the end of the stream), where the string before the
101     * line separator is the string representation of a {@code double}, and
102     * returns that {@code double}.
103     *
104     * @return the {@code double} read
105     * @updates this.content
106     * @requires {@code
107     * this.is_open  and
108     * there exists d: real
109     *   (Double.MIN_VALUE <= d  and  d <= Double.MAX_VALUE  and
110     *    (TO_STRING(d) * LINE_SEPARATOR is prefix of this.content  or
111     *     TO_STRING(d) = this.content))
112     * }
113     * @ensures {@code
114     * if LINE_SEPARATOR is substring of #this.content
115     *   then (#this.content = TO_STRING(nextDouble) * LINE_SEPARATOR * this.content)
116     *   else (TO_STRING(nextDouble) = #this.content  and  this.content = <>)
117     * }
118     */
119    double nextDouble();
120
121}