Interface ProgramKernel

All Superinterfaces:
Standard<Program>
All Known Subinterfaces:
Program
All Known Implementing Classes:
Program1, ProgramSecondary
public interface ProgramKernel extends Standard<Program>
Program kernel component with kernel methods. (Note: by package-wide convention, all references are non-null.)
Mathematical Subtypes:
CONTEXT is finite set of (name: IDENTIFIER, body: STATEMENT_MODEL)
exemplar c
constraint
 [the names of instructions in c are unique]  and
 [the names of instructions in c do not match the names of primitive
  instructions in the BL language]  and
 [the bodies of instructions in c are all BLOCK statements]

PROGRAM_MODEL is (
 name: IDENTIFIER,
 context: CONTEXT,
 body: STATEMENT_MODEL
)
exemplar p
constraint
 [p.body is a BLOCK statement]
Mathematical Model (abstract value and abstract invariant of this):
type ProgramKernel is modeled by PROGRAM_MODEL
Constructor(s) (initial abstract value(s) of this):
():
ensures
 this = ("Unnamed", {}, compose((BLOCK, ?, ?), <>))

  • Method Summary

    Modifier and Type
    Method
    Description
    String
    name()
    Returns the name of this.
    Statement
    newBody()
    Creates and returns a Statement with a default initial value, of the dynamic type needed in swapBody.
    Map<String, Statement>
    newContext()
    Creates and returns an empty Map<String, Statement> of the dynamic type needed in swapContext.
    void
    setName(String n)
    Replaces the name of this with n.
    void
    swapBody(Statement b)
    Exchanges the body of this with b; b must have the dynamic type returned by newBody.
    void
    swapContext(Map<String, Statement> c)
    Exchanges the context of this with c; c must have the dynamic type returned by newContext.

    Methods inherited from interface Standard

    clear, newInstance, transferFrom

  • Method Details

    • name

      String name()
      Returns the name of this.
      Returns:
      the name of this
      Ensures:
      name = this.name

    • setName

      void setName(String n)
      Replaces the name of this with n.
      Parameters:
      n - the name replacing the old one
      Replaces:
      this.name
      Requires:
      [n is a valid IDENTIFIER]
      Ensures:
      this.name = n

    • newContext

      Map<String, Statement> newContext()
      Creates and returns an empty Map<String, Statement> of the dynamic type needed in swapContext.
      Returns:
      a new empty Map<String, Statement>
      Ensures:
      newContext = {}

    • swapContext

      void swapContext(Map<String, Statement> c)
      Exchanges the context of this with c; c must have the dynamic type returned by newContext.
      Parameters:
      c - the context to be exchanged with that of this
      Updates:
      this.context, c
      Requires:
      [names in c are valid IDENTIFIERs]  and
[names in c do not match the names of primitive instructions
in the BL language]  and
[bodies in c are all BLOCK statements]
      Ensures:
      this.context = #c and c = #this.context

    • newBody

      Statement newBody()
      Creates and returns a Statement with a default initial value, of the dynamic type needed in swapBody.
      Returns:
      a new Statement
      Ensures:
      newBody = compose((BLOCK, ?, ?), <>)

    • swapBody

      void swapBody(Statement b)
      Exchanges the body of this with b; b must have the dynamic type returned by newBody.
      Parameters:
      b - the body to be exchanged with that of this
      Updates:
      this.body, b
      Requires:
      [b is a BLOCK statement]
      Ensures:
      this.body = #b and b = #this.body