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, NEXT_IS_NOT_FRIEND, NEXT_IS_ENEMY, NEXT_IS_NOT_ENEMY, RANDOM, TRUE
062    }
063
064    /**
065     * Reports the kind of statement {@code this} is.
066     *
067     * @return the kind of this statement
068     * @ensures kind = [the kind of this statement]
069     */
070    Kind kind();
071
072    /**
073     * Adds the statement {@code s} at position {@code pos} in {@code this}
074     * BLOCK statement; the declaration notwithstanding, the <i>dynamic</i> type
075     * of {@code s} must be the same as the <i>dynamic</i> type of {@code this}.
076     *
077     * @param pos
078     *            the position at which to add {@code s}
079     * @param s
080     *            the {@code Statement} to add
081     * @updates this
082     * @clears s
083     * @requires {@code
084     * [this is a BLOCK statement]  and
085     * [s is not a BLOCK statement]  and
086     * 0 <= pos <= [length of this BLOCK]
087     * }
088     * @ensures this = [#this with child #s inserted at position pos]
089     */
090    void addToBlock(int pos, Statement s);
091
092    /**
093     * Removes and returns the statement at position {@code pos} in {@code this}
094     * BLOCK statement.
095     *
096     * @param pos
097     *            the position of the child to remove
098     * @return the child at position pos in {@code this}
099     * @updates this
100     * @requires {@code
101     * [this is a BLOCK statement]  and
102     * 0 <= pos < [length of this BLOCK]
103     * }
104     * @ensures <pre>
105     * this =
106     *  [#this with child at position pos removed and returned as result]
107     * </pre>
108     */
109    Statement removeFromBlock(int pos);
110
111    /**
112     * Reports the number of statements in {@code this} BLOCK.
113     *
114     * @return the length of {@code this} BLOCK
115     * @requires [this is a BLOCK statement]
116     * @ensures lengthOfBlock = [the number of children of this]
117     */
118    int lengthOfBlock();
119
120    /**
121     * Assembles in {@code this} an IF statement with root label
122     * {@code (IF, c, ?)} and only subtree the BLOCK {@code s}; the declaration
123     * notwithstanding, the <i>dynamic</i> type of {@code s} must be the same as
124     * the <i>dynamic</i> type of {@code this}.
125     *
126     * @param c
127     *            the {@code Condition} of the IF statement
128     * @param s
129     *            the body of the IF statement
130     * @replaces this
131     * @clears s
132     * @requires [s is a BLOCK statement]
133     * @ensures {@code this = compose((IF, c, ?), <#s>)}
134     */
135    void assembleIf(Condition c, Statement s);
136
137    /**
138     * Disassembles IF statement {@code this} into its test {@code Condition},
139     * which is returned as the value of the function, and its only subtree, the
140     * BLOCK statement {@code s}; the declaration notwithstanding, the
141     * <i>dynamic</i> type of {@code s} must be the same as the <i>dynamic</i>
142     * type of {@code this}.
143     *
144     * @param s
145     *            the body of this IF statement
146     * @return the {@code Condition} of this IF statement
147     * @clears this
148     * @replaces s
149     * @requires [this is an IF statement]
150     * @ensures {@code #this = compose((IF, disassembleIf, ?), <s>)}
151     */
152    Condition disassembleIf(Statement s);
153
154    /**
155     * Assembles in {@code this} an IF_ELSE statement with root label
156     * {@code (IF_ELSE, c, ?)} and as two subtrees the BLOCKs {@code s1} and
157     * {@code s2}; the declaration notwithstanding, the <i>dynamic</i> type of
158     * {@code s1} and {@code s2} must be the same as the <i>dynamic</i> type of
159     * {@code this}.
160     *
161     * @param c
162     *            the {@code Condition} of the IF_ELSE statement
163     * @param s1
164     *            the body of the "then" part of the IF_ELSE statement
165     * @param s2
166     *            the body of the "else" part of the IF_ELSE statement
167     * @replaces this
168     * @clears s1, s2
169     * @requires <pre>
170     * [s1 is a BLOCK statement]  and
171     * [s2 is a BLOCK statement]
172     * </pre>
173     * @ensures {@code this = compose((IF_ELSE, c, ?), <#s1, #s2>)}
174     */
175    void assembleIfElse(Condition c, Statement s1, Statement s2);
176
177    /**
178     * Disassembles IF_ELSE statement {@code this} into its test
179     * {@code Condition}, which is returned as the value of the function, and
180     * its two subtrees, the BLOCK statements {@code s1} and {@code s2}; the
181     * declaration notwithstanding, the <i>dynamic</i> type of {@code s1} and
182     * {@code s2} must be the same as the <i>dynamic</i> type of {@code this}.
183     *
184     * @param s1
185     *            the body of the "then" part of the IF_ELSE statement
186     * @param s2
187     *            the body of the "else" part of the IF_ELSE statement
188     * @return the {@code Condition} of this IF_ELSE statement
189     * @clears this
190     * @replaces s1, s2
191     * @requires [this is an IF_ELSE statement]
192     * @ensures {@code #this = compose((IF_ELSE, disassembleIfElse, ?), <s1, s2>)}
193     */
194    Condition disassembleIfElse(Statement s1, Statement s2);
195
196    /**
197     * Assembles in {@code this} a WHILE statement with root label
198     * {@code (WHILE, c, ?)} and only subtree the BLOCK {@code s}; the
199     * declaration notwithstanding, the <i>dynamic</i> type of {@code s} must be
200     * the same as the <i>dynamic</i> type of {@code this}.
201     *
202     * @param c
203     *            the {@code Condition} of the WHILE statement
204     * @param s
205     *            the body of the WHILE statement
206     * @replaces this
207     * @clears s
208     * @requires [s is a BLOCK statement]
209     * @ensures {@code this = compose((WHILE, c, ?), <#s>)}
210     */
211    void assembleWhile(Condition c, Statement s);
212
213    /**
214     * Disassembles WHILE statement {@code this} into its test {@code Condition}
215     * , which is returned as the value of the function, and its only subtree,
216     * the BLOCK statement {@code s}; the declaration notwithstanding, the
217     * <i>dynamic</i> type of {@code s} must be the same as the <i>dynamic</i>
218     * type of {@code this}.
219     *
220     * @param s
221     *            the body of this WHILE statement
222     * @return the {@code Condition} of this WHILE statement
223     * @clears this
224     * @replaces s
225     * @requires [this is a WHILE statement]
226     * @ensures {@code #this = compose((WHILE, disassembleWhile, ?), <s>)}
227     */
228    Condition disassembleWhile(Statement s);
229
230    /**
231     * Assembles in {@code this} a CALL statement with root label
232     * {@code (CALL, ?, inst)} and no subtrees.
233     *
234     * @param inst
235     *            the name of the instruction of the CALL statement
236     * @replaces this
237     * @requires [inst is a valid IDENTIFIER]
238     * @ensures {@code this = compose((CALL, ?, inst), <>)}
239     */
240    void assembleCall(String inst);
241
242    /**
243     * Disassembles CALL statement {@code this} and returns the called
244     * instruction name as the value of the function.
245     *
246     * @return the name of the instruction of this CALL statement
247     * @clears this
248     * @requires [this is a CALL statement]
249     * @ensures {@code #this = compose((CALL, ?, disassembleCall), <>)}
250     */
251    String disassembleCall();
252
253}