001package components.program;
002
003import components.map.Map;
004import components.standard.Standard;
005import components.statement.Statement;
006
007/**
008 * Program kernel component with kernel methods. (Note: by package-wide
009 * convention, all references are non-null.) <br/>
010 *
011 * @mathsubtypes <pre>
012 * CONTEXT is finite set of (name: IDENTIFIER, body: STATEMENT_MODEL)
013 *  exemplar c
014 *  constraint
015 *   [the names of instructions in c are unique]  and
016 *   [the names of instructions in c do not match the names of primitive
017 *    instructions in the BL language]  and
018 *   [the bodies of instructions in c are all BLOCK statements]
019 *
020 * PROGRAM_MODEL is (
021 *   name: IDENTIFIER,
022 *   context: CONTEXT,
023 *   body: STATEMENT_MODEL
024 *  )
025 *  exemplar p
026 *  constraint
027 *   [p.body is a BLOCK statement]
028 * </pre>
029 * @mathmodel type ProgramKernel is modeled by PROGRAM_MODEL
030 * @initially {@code <pre>
031 * ():
032 *  ensures
033 *   this = ("Unnamed", {}, compose((BLOCK, ?, ?), <>))
034 * </pre>  }
035 */
036public interface ProgramKernel extends Standard<Program> {
037
038    /**
039     * Returns the name of {@code this}.
040     *
041     * @return the name of {@code this}
042     * @ensures name = this.name
043     */
044    String name();
045
046    /**
047     * Replaces the name of {@code this} with {@code n}.
048     *
049     * @param n
050     *            the name replacing the old one
051     * @replaces this.name
052     * @requires [n is a valid IDENTIFIER]
053     * @ensures this.name = n
054     */
055    void setName(String n);
056
057    /**
058     * Creates and returns an empty {@code Map<String, Statement>} of the
059     * dynamic type needed in {@code swapContext}.
060     *
061     * @return a new empty {@code Map<String, Statement>}
062     * @ensures newContext = {}
063     */
064    Map<String, Statement> newContext();
065
066    /**
067     * Exchanges the context of {@code this} with {@code c}; {@code c} must have
068     * the dynamic type returned by {@code newContext}.
069     *
070     * @param c
071     *            the context to be exchanged with that of {@code this}
072     * @updates this.context, c
073     * @requires <pre>
074     * [names in c are valid IDENTIFIERs]  and
075     * [names in c do not match the names of primitive instructions
076     *  in the BL language]  and
077     * [bodies in c are all BLOCK statements]
078     * </pre>
079     * @ensures this.context = #c and c = #this.context
080     */
081    void swapContext(Map<String, Statement> c);
082
083    /**
084     * Creates and returns a {@code Statement} with a default initial value, of
085     * the dynamic type needed in {@code swapBody}.
086     *
087     * @return a new {@code Statement}
088     * @ensures {@code newBody = compose((BLOCK, ?, ?), <>)}
089     */
090    Statement newBody();
091
092    /**
093     * Exchanges the body of {@code this} with {@code b}; {@code b} must have
094     * the dynamic type returned by {@code newBody}.
095     *
096     * @param b
097     *            the body to be exchanged with that of {@code this}
098     * @updates this.body, b
099     * @requires [b is a BLOCK statement]
100     * @ensures this.body = #b and b = #this.body
101     */
102    void swapBody(Statement b);
103
104}