001package components.simplewriter;
002
003/**
004 * {@code SimpleWriterKernel} 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 local system]
009 * </pre>
010 */
011public interface SimpleWriter extends SimpleWriterKernel {
012
013    /**
014     * Appends {@code s} to the end of {@code this.content}.
015     *
016     * @param s
017     *            the string to output
018     * @updates this.content
019     * @requires this.is_open
020     * @ensures this.content = #this.content * s
021     */
022    void print(String s);
023
024    /**
025     * Appends {@code TO_STRING(i)} to the end of {@code this.content}.
026     *
027     * @param i
028     *            the integer to output
029     * @updates this.content
030     * @requires this.is_open
031     * @ensures this.content = #this.content * TO_STRING(i)
032     */
033    void print(int i);
034
035    /**
036     * Appends {@code TO_STRING(x)} to the end of {@code this.content}.
037     *
038     * @param x
039     *            the long to output
040     * @updates this.content
041     * @requires this.is_open
042     * @ensures this.content = #this.content * TO_STRING(x)
043     */
044    void print(long x);
045
046    /**
047     * Appends {@code TO_STRING(d)} to the end of {@code this.content}.
048     *
049     * @param d
050     *            the double to output
051     * @updates this.content
052     * @requires this.is_open
053     * @ensures this.content = #this.content * TO_STRING(d)
054     */
055    void print(double d);
056
057    /**
058     * Appends {@code TO_STRING(d, precision, scientific)} to the end of
059     * {@code this.content}.
060     *
061     * @param d
062     *            the double to output
063     * @param precision
064     *            the number of decimal digits printed
065     * @param scientific
066     *            whether to use scientific notation or not
067     * @updates this.content
068     * @requires this.is_open and precision >= 0
069     * @ensures <pre>
070     * this.content = #this.content * TO_STRING(d, precision, scientific)
071     * </pre>
072     */
073    void print(double d, int precision, boolean scientific);
074
075    /**
076     * Appends {@code TO_STRING(b)} to the end of {@code this.content}.
077     *
078     * @param b
079     *            the boolean to output
080     * @updates this.content
081     * @requires this.is_open
082     * @ensures this.content = #this.content * TO_STRING(b)
083     */
084    void print(boolean b);
085
086    /**
087     * Appends {@code <c>} to the end of {@code this.content}.
088     *
089     * @param c
090     *            the character to output
091     * @updates this.content
092     * @requires this.is_open
093     * @ensures {@code this.content = #this.content * <c>}
094     */
095    void print(char c);
096
097    /**
098     * Appends the string representation of {@code o} to the end of
099     * {@code this.content}.
100     *
101     * @param o
102     *            the Object to output
103     * @updates this.content
104     * @requires this.is_open
105     * @ensures this.content = #this.content * to_string(o)
106     */
107    void print(Object o);
108
109    /**
110     * Appends {@code s} and a line separator to the end of {@code this.content}
111     * .
112     *
113     * @param s
114     *            the string to output
115     * @updates this.content
116     * @requires this.is_open
117     * @ensures this.content = #this.content * s * LINE_SEPARATOR
118     */
119    void println(String s);
120
121    /**
122     * Appends {@code TO_STRING(i)} and a line separator to the end of
123     * {@code this.content}.
124     *
125     * @param i
126     *            the integer to output
127     * @updates this.content
128     * @requires this.is_open
129     * @ensures this.content = #this.content * TO_STRING(i) * LINE_SEPARATOR
130     */
131    void println(int i);
132
133    /**
134     * Appends {@code TO_STRING(x)} and a line separator to the end of
135     * {@code this.content}.
136     *
137     * @param x
138     *            the long to output
139     * @updates this.content
140     * @requires this.is_open
141     * @ensures this.content = #this.content * TO_STRING(x) * LINE_SEPARATOR
142     */
143    void println(long x);
144
145    /**
146     * Appends {@code TO_STRING(d)} and a line separator to the end of
147     * {@code this.content}.
148     *
149     * @param d
150     *            the double to output
151     * @updates this.content
152     * @requires this.is_open
153     * @ensures this.content = #this.content * TO_STRING(d) * LINE_SEPARATOR
154     */
155    void println(double d);
156
157    /**
158     * Appends {@code TO_STRING(d, precision, scientific)} and a line separator
159     * to the end of {@code this.content}.
160     *
161     * @param d
162     *            the double to output
163     * @param precision
164     *            the number of decimal digits printed
165     * @param scientific
166     *            whether to use scientific notation or not
167     * @updates this.content
168     * @requires this.is_open and precision >= 0
169     * @ensures <pre>
170     * this.content =
171     *   #this.content * TO_STRING(d, precision, scientific) * LINE_SEPARATOR
172     * </pre>
173     */
174    void println(double d, int precision, boolean scientific);
175
176    /**
177     * Appends {@code TO_STRING(b)} and a line separator to the end of
178     * {@code this.content}.
179     *
180     * @param b
181     *            the boolean to output
182     * @updates this.content
183     * @requires this.is_open
184     * @ensures this.content = #this.content * TO_STRING(b) * LINE_SEPARATOR
185     */
186    void println(boolean b);
187
188    /**
189     * Appends {@code <c>} and a line separator to the end of
190     * {@code this.content}.
191     *
192     * @param c
193     *            the character to output
194     * @updates this.content
195     * @requires this.is_open
196     * @ensures {@code this.content = #this.content * <c> * LINE_SEPARATOR}
197     */
198    void println(char c);
199
200    /**
201     * Appends a line separator to the end of {@code this.content}.
202     *
203     * @updates this.content
204     * @requires this.is_open
205     * @ensures this.content = #this.content * LINE_SEPARATOR
206     */
207    void println();
208
209    /**
210     * Appends the string representation of {@code o} and a line separator to
211     * the end of {@code this.content}.
212     *
213     * @param o
214     *            the Object to output
215     * @updates this.content
216     * @requires this.is_open
217     * @ensures this.content = #this.content * to_string(o) * LINE_SEPARATOR
218     */
219    void println(Object o);
220
221}