001package components.statement;
002
003import components.standard.Standard;
004
005/**
006 * Statement kernel component with kernel methods. (Note: by package-wide
007 * convention, all references are non-null.) <br/>
008 *
009 * @mathsubtypes <pre>
010 * IDENTIFIER is string of character
011 *  exemplar id
012 *  constraint
013 *   [id starts with a letter 'a'-'z', 'A'-'Z']  and
014 *   [id contains only letters, digits '0'-'9', and '-']  and
015 *   [id is not one of the keywords or conditions in the BL language]
016 *
017 * STATEMENT_LABEL is (
018 *   kind: Kind,
019 *   test: Condition,
020 *   call: IDENTIFIER
021 *  )
022 *  exemplar sl
023 *  constraint
024 *   [if sl.kind = BLOCK then sl.test and sl.call are irrelevant]  and
025 *   [if sl.kind = IF or sl.kind = IF_ELSE or sl.kind = WHILE
026 *    then sl.call is irrelevant]  and
027 *   [if sl.kind = CALL then sl.test is irrelevant]
028 *
029 * STATEMENT_MODEL is tree of STATEMENT_LABEL
030 *  exemplar s
031 *  constraint
032 *   |s| > 0  and
033 *   [BLOCK can have 0 or more children, but not another BLOCK as a child]  and
034 *   [IF must have exactly one BLOCK child]  and
035 *   [IF_ELSE must have exactly two BLOCK children]  and
036 *   [WHILE must have exactly one BLOCK child]  and
037 *   [CALL must have no children (must be a leaf)]
038 * </pre>
039 * @mathmodel type StatementKernel is modeled by STATEMENT_MODEL
040 * @initially {@code
041 * ():
042 *  ensures
043 *   this = compose((BLOCK, ?, ?), <>)
044 * }
045 */
046public interface StatementKernel extends Standard<Statement> {
047
048    /**
049     * The kinds of statements.
050     */
051    enum Kind {
052        // SUPPRESS CHECKSTYLE Javadoc FOR NEXT 5 LINES
053        BLOCK, IF, IF_ELSE, WHILE, CALL
054    }
055
056    /**
057     * The possible conditions for IF, IF_ELSE, and WHILE statements.
058     */
059    enum Condition {
060        // SUPPRESS CHECKSTYLE Javadoc FOR NEXT 10 LINES
061        NEXT_IS_EMPTY, NEXT_IS_NOT_EMPTY, NEXT_IS_WALL, NEXT_IS_NOT_WALL, NEXT_IS_FRIEND,
062        NEXT_IS_NOT_FRIEND, NEXT_IS_ENEMY, NEXT_IS_NOT_ENEMY, RANDOM, TRUE
063    }
064
065    /**
066     * Reports the kind of statement {@code this} is.
067     *
068     * @return the kind of this statement
069     * @ensures kind = [the kind of this statement]
070     */
071    Kind kind();
072
073    /**
074     * Adds the statement {@code s} at position {@code pos} in {@code this}
075     * BLOCK statement; the declaration notwithstanding, the <i>dynamic</i> type
076     * of {@code s} must be the same as the <i>dynamic</i> type of {@code this}.
077     *
078     * @param pos
079     *            the position at which to add {@code s}
080     * @param s
081     *            the {@code Statement} to add
082     * @updates this
083     * @clears s
084     * @requires {@code
085     * [this is a BLOCK statement]  and
086     * [s is not a BLOCK statement]  and
087     * 0 <= pos <= [length of this BLOCK]
088     * }
089     * @ensures this = [#this with child #s inserted at position pos]
090     */
091    void addToBlock(int pos, Statement s);
092
093    /**
094     * Removes and returns the statement at position {@code pos} in {@code this}
095     * BLOCK statement.
096     *
097     * @param pos
098     *            the position of the child to remove
099     * @return the child at position pos in {@code this}
100     * @updates this
101     * @requires {@code
102     * [this is a BLOCK statement]  and
103     * 0 <= pos < [length of this BLOCK]
104     * }
105     * @ensures <pre>
106     * this =
107     *  [#this with child at position pos removed and returned as result]
108     * </pre>
109     */
110    Statement removeFromBlock(int pos);
111
112    /**
113     * Reports the number of statements in {@code this} BLOCK.
114     *
115     * @return the length of {@code this} BLOCK
116     * @requires [this is a BLOCK statement]
117     * @ensures lengthOfBlock = [the number of children of this]
118     */
119    int lengthOfBlock();
120
121    /**
122     * Assembles in {@code this} an IF statement with root label
123     * {@code (IF, c, ?)} and only subtree the BLOCK {@code s}; the declaration
124     * notwithstanding, the <i>dynamic</i> type of {@code s} must be the same as
125     * the <i>dynamic</i> type of {@code this}.
126     *
127     * @param c
128     *            the {@code Condition} of the IF statement
129     * @param s
130     *            the body of the IF statement
131     * @replaces this
132     * @clears s
133     * @requires [s is a BLOCK statement]
134     * @ensures {@code this = compose((IF, c, ?), <#s>)}
135     */
136    void assembleIf(Condition c, Statement s);
137
138    /**
139     * Disassembles IF statement {@code this} into its test {@code Condition},
140     * which is returned as the value of the function, and its only subtree, the
141     * BLOCK statement {@code s}; the declaration notwithstanding, the
142     * <i>dynamic</i> type of {@code s} must be the same as the <i>dynamic</i>
143     * type of {@code this}.
144     *
145     * @param s
146     *            the body of this IF statement
147     * @return the {@code Condition} of this IF statement
148     * @clears this
149     * @replaces s
150     * @requires [this is an IF statement]
151     * @ensures {@code #this = compose((IF, disassembleIf, ?), <s>)}
152     */
153    Condition disassembleIf(Statement s);
154
155    /**
156     * Assembles in {@code this} an IF_ELSE statement with root label
157     * {@code (IF_ELSE, c, ?)} and as two subtrees the BLOCKs {@code s1} and
158     * {@code s2}; the declaration notwithstanding, the <i>dynamic</i> type of
159     * {@code s1} and {@code s2} must be the same as the <i>dynamic</i> type of
160     * {@code this}.
161     *
162     * @param c
163     *            the {@code Condition} of the IF_ELSE statement
164     * @param s1
165     *            the body of the "then" part of the IF_ELSE statement
166     * @param s2
167     *            the body of the "else" part of the IF_ELSE statement
168     * @replaces this
169     * @clears s1, s2
170     * @requires <pre>
171     * [s1 is a BLOCK statement]  and
172     * [s2 is a BLOCK statement]
173     * </pre>
174     * @ensures {@code this = compose((IF_ELSE, c, ?), <#s1, #s2>)}
175     */
176    void assembleIfElse(Condition c, Statement s1, Statement s2);
177
178    /**
179     * Disassembles IF_ELSE statement {@code this} into its test
180     * {@code Condition}, which is returned as the value of the function, and
181     * its two subtrees, the BLOCK statements {@code s1} and {@code s2}; the
182     * declaration notwithstanding, the <i>dynamic</i> type of {@code s1} and
183     * {@code s2} must be the same as the <i>dynamic</i> type of {@code this}.
184     *
185     * @param s1
186     *            the body of the "then" part of the IF_ELSE statement
187     * @param s2
188     *            the body of the "else" part of the IF_ELSE statement
189     * @return the {@code Condition} of this IF_ELSE statement
190     * @clears this
191     * @replaces s1, s2
192     * @requires [this is an IF_ELSE statement]
193     * @ensures {@code #this = compose((IF_ELSE, disassembleIfElse, ?), <s1, s2>)}
194     */
195    Condition disassembleIfElse(Statement s1, Statement s2);
196
197    /**
198     * Assembles in {@code this} a WHILE statement with root label
199     * {@code (WHILE, c, ?)} and only subtree the BLOCK {@code s}; the
200     * declaration notwithstanding, the <i>dynamic</i> type of {@code s} must be
201     * the same as the <i>dynamic</i> type of {@code this}.
202     *
203     * @param c
204     *            the {@code Condition} of the WHILE statement
205     * @param s
206     *            the body of the WHILE statement
207     * @replaces this
208     * @clears s
209     * @requires [s is a BLOCK statement]
210     * @ensures {@code this = compose((WHILE, c, ?), <#s>)}
211     */
212    void assembleWhile(Condition c, Statement s);
213
214    /**
215     * Disassembles WHILE statement {@code this} into its test {@code Condition}
216     * , which is returned as the value of the function, and its only subtree,
217     * the BLOCK statement {@code s}; the declaration notwithstanding, the
218     * <i>dynamic</i> type of {@code s} must be the same as the <i>dynamic</i>
219     * type of {@code this}.
220     *
221     * @param s
222     *            the body of this WHILE statement
223     * @return the {@code Condition} of this WHILE statement
224     * @clears this
225     * @replaces s
226     * @requires [this is a WHILE statement]
227     * @ensures {@code #this = compose((WHILE, disassembleWhile, ?), <s>)}
228     */
229    Condition disassembleWhile(Statement s);
230
231    /**
232     * Assembles in {@code this} a CALL statement with root label
233     * {@code (CALL, ?, inst)} and no subtrees.
234     *
235     * @param inst
236     *            the name of the instruction of the CALL statement
237     * @replaces this
238     * @requires [inst is a valid IDENTIFIER]
239     * @ensures {@code this = compose((CALL, ?, inst), <>)}
240     */
241    void assembleCall(String inst);
242
243    /**
244     * Disassembles CALL statement {@code this} and returns the called
245     * instruction name as the value of the function.
246     *
247     * @return the name of the instruction of this CALL statement
248     * @clears this
249     * @requires [this is a CALL statement]
250     * @ensures {@code #this = compose((CALL, ?, disassembleCall), <>)}
251     */
252    String disassembleCall();
253
254}