All Superinterfaces:: Standard<Statement>

All Known Subinterfaces:: Statement

All Known Implementing Classes:: Statement1, StatementSecondary

public interface StatementKernel extends Standard<Statement>

Statement kernel component with kernel methods. (Note: by package-wide convention, all references are non-null.)

Mathematical Subtypes:

IDENTIFIER is string of character
 exemplar id
 constraint
  [id starts with a letter 'a'-'z', 'A'-'Z']  and
  [id contains only letters, digits '0'-'9', and '-']  and
  [id is not one of the keywords or conditions in the BL language]

STATEMENT_LABEL is (
  kind: Kind,
  test: Condition,
  call: IDENTIFIER
 )
 exemplar sl
 constraint
  [if sl.kind = BLOCK then sl.test and sl.call are irrelevant]  and
  [if sl.kind = IF or sl.kind = IF_ELSE or sl.kind = WHILE
   then sl.call is irrelevant]  and
  [if sl.kind = CALL then sl.test is irrelevant]

STATEMENT_MODEL is tree of STATEMENT_LABEL
 exemplar s
 constraint
  |s| > 0  and
  [BLOCK can have 0 or more children, but not another BLOCK as a child]  and
  [IF must have exactly one BLOCK child]  and
  [IF_ELSE must have exactly two BLOCK children]  and
  [WHILE must have exactly one BLOCK child]  and
  [CALL must have no children (must be a leaf)]

Mathematical Model (abstract value and abstract invariant of this):

type StatementKernel is modeled by STATEMENT_MODEL

Constructor(s) (initial abstract value(s) of this):

():
 ensures
  this = compose((BLOCK, ?, ?), <>)

Nested Class Summary

Nested Classes

Modifier and Type

Interface

Description

static enum

StatementKernel.Condition

The possible conditions for IF, IF_ELSE, and WHILE statements.

static enum

StatementKernel.Kind

The kinds of statements.
Method Summary

Modifier and Type

Method

Description

void

addToBlock(int pos, Statement s)

Adds the statement s at position pos in this BLOCK statement; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.

void

assembleCall(String inst)

Assembles in this a CALL statement with root label (CALL, ?, inst) and no subtrees.

void

assembleIf(StatementKernel.Condition c, Statement s)

Assembles in this an IF statement with root label (IF, c, ?) and only subtree the BLOCK s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.

void

assembleIfElse(StatementKernel.Condition c, Statement s1, Statement s2)

Assembles in this an IF_ELSE statement with root label (IF_ELSE, c, ?) and as two subtrees the BLOCKs s1 and s2; the declaration notwithstanding, the dynamic type of s1 and s2 must be the same as the dynamic type of this.

void

assembleWhile(StatementKernel.Condition c, Statement s)

Assembles in this a WHILE statement with root label (WHILE, c, ?) and only subtree the BLOCK s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.

String

disassembleCall()

Disassembles CALL statement this and returns the called instruction name as the value of the function.

StatementKernel.Condition

disassembleIf(Statement s)

Disassembles IF statement this into its test Condition, which is returned as the value of the function, and its only subtree, the BLOCK statement s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.

StatementKernel.Condition

disassembleIfElse(Statement s1, Statement s2)

Disassembles IF_ELSE statement this into its test Condition, which is returned as the value of the function, and its two subtrees, the BLOCK statements s1 and s2; the declaration notwithstanding, the dynamic type of s1 and s2 must be the same as the dynamic type of this.

StatementKernel.Condition

disassembleWhile(Statement s)

Disassembles WHILE statement this into its test Condition , which is returned as the value of the function, and its only subtree, the BLOCK statement s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.

StatementKernel.Kind

kind()

Reports the kind of statement this is.

int

lengthOfBlock()

Reports the number of statements in this BLOCK.

Statement

removeFromBlock(int pos)

Removes and returns the statement at position pos in this BLOCK statement.

Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom

Method Details
- kind
  
  StatementKernel.Kind kind()
  
  Reports the kind of statement this is.
  Returns:
  
  the kind of this statement
  
  Ensures:
  
  kind = [the kind of this statement]
- addToBlock
  
  void addToBlock(int pos, Statement s)
  
  Adds the statement s at position pos in this BLOCK statement; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.
  Parameters:
  
  pos - the position at which to add s
  
  s - the Statement to add
  
  Updates:
  
  this
  
  Clears:
  
  s
  
  Requires:
  
  [this is a BLOCK statement] and [s is not a BLOCK statement] and 0 <= pos <= [length of this BLOCK]
  
  Ensures:
  
  this = [#this with child #s inserted at position pos]
- removeFromBlock
  
  Statement removeFromBlock(int pos)
  
  Removes and returns the statement at position pos in this BLOCK statement.
  Parameters:
  
  pos - the position of the child to remove
  
  Returns:
  
  the child at position pos in this
  
  Updates:
  
  this
  
  Requires:
  
  [this is a BLOCK statement] and 0 <= pos < [length of this BLOCK]
  
  Ensures:
  
  this = [#this with child at position pos removed and returned as result]
- lengthOfBlock
  
  int lengthOfBlock()
  
  Reports the number of statements in this BLOCK.
  Returns:
  
  the length of this BLOCK
  
  Requires:
  
  [this is a BLOCK statement]
  
  Ensures:
  
  lengthOfBlock = [the number of children of this]
- assembleIf
  
  void assembleIf(StatementKernel.Condition c, Statement s)
  
  Assembles in this an IF statement with root label (IF, c, ?) and only subtree the BLOCK s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.
  Parameters:
  
  c - the Condition of the IF statement
  
  s - the body of the IF statement
  
  Replaces:
  
  this
  
  Clears:
  
  s
  
  Requires:
  
  [s is a BLOCK statement]
  
  Ensures:
  
  this = compose((IF, c, ?), <#s>)
- disassembleIf
  
  StatementKernel.Condition disassembleIf(Statement s)
  
  Disassembles IF statement this into its test Condition, which is returned as the value of the function, and its only subtree, the BLOCK statement s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.
  Parameters:
  
  s - the body of this IF statement
  
  Returns:
  
  the Condition of this IF statement
  
  Replaces:
  
  s
  
  Clears:
  
  this
  
  Requires:
  
  [this is an IF statement]
  
  Ensures:
  
  #this = compose((IF, disassembleIf, ?), <s>)
- assembleIfElse
  
  void assembleIfElse(StatementKernel.Condition c, Statement s1, Statement s2)
  
  Assembles in this an IF_ELSE statement with root label (IF_ELSE, c, ?) and as two subtrees the BLOCKs s1 and s2; the declaration notwithstanding, the dynamic type of s1 and s2 must be the same as the dynamic type of this.
  Parameters:
  
  c - the Condition of the IF_ELSE statement
  
  s1 - the body of the "then" part of the IF_ELSE statement
  
  s2 - the body of the "else" part of the IF_ELSE statement
  
  Replaces:
  
  this
  
  Clears:
  
  s1, s2
  
  Requires:
  
  [s1 is a BLOCK statement] and [s2 is a BLOCK statement]
  
  Ensures:
  
  this = compose((IF_ELSE, c, ?), <#s1, #s2>)
- disassembleIfElse
  
  StatementKernel.Condition disassembleIfElse(Statement s1, Statement s2)
  
  Disassembles IF_ELSE statement this into its test Condition, which is returned as the value of the function, and its two subtrees, the BLOCK statements s1 and s2; the declaration notwithstanding, the dynamic type of s1 and s2 must be the same as the dynamic type of this.
  Parameters:
  
  s1 - the body of the "then" part of the IF_ELSE statement
  
  s2 - the body of the "else" part of the IF_ELSE statement
  
  Returns:
  
  the Condition of this IF_ELSE statement
  
  Replaces:
  
  s1, s2
  
  Clears:
  
  this
  
  Requires:
  
  [this is an IF_ELSE statement]
  
  Ensures:
  
  #this = compose((IF_ELSE, disassembleIfElse, ?), <s1, s2>)
- assembleWhile
  
  void assembleWhile(StatementKernel.Condition c, Statement s)
  
  Assembles in this a WHILE statement with root label (WHILE, c, ?) and only subtree the BLOCK s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.
  Parameters:
  
  c - the Condition of the WHILE statement
  
  s - the body of the WHILE statement
  
  Replaces:
  
  this
  
  Clears:
  
  s
  
  Requires:
  
  [s is a BLOCK statement]
  
  Ensures:
  
  this = compose((WHILE, c, ?), <#s>)
- disassembleWhile
  
  StatementKernel.Condition disassembleWhile(Statement s)
  
  Disassembles WHILE statement this into its test Condition , which is returned as the value of the function, and its only subtree, the BLOCK statement s; the declaration notwithstanding, the dynamic type of s must be the same as the dynamic type of this.
  Parameters:
  
  s - the body of this WHILE statement
  
  Returns:
  
  the Condition of this WHILE statement
  
  Replaces:
  
  s
  
  Clears:
  
  this
  
  Requires:
  
  [this is a WHILE statement]
  
  Ensures:
  
  #this = compose((WHILE, disassembleWhile, ?), <s>)
- assembleCall
  
  void assembleCall(String inst)
  
  Assembles in this a CALL statement with root label (CALL, ?, inst) and no subtrees.
  Parameters:
  
  inst - the name of the instruction of the CALL statement
  
  Replaces:
  
  this
  
  Requires:
  
  [inst is a valid IDENTIFIER]
  
  Ensures:
  
  this = compose((CALL, ?, inst), <>)
- disassembleCall
  
  String disassembleCall()
  
  Disassembles CALL statement this and returns the called instruction name as the value of the function.
  Returns:
  
  the name of the instruction of this CALL statement
  
  Clears:
  
  this
  
  Requires:
  
  [this is a CALL statement]
  
  Ensures:
  
  #this = compose((CALL, ?, disassembleCall), <>)

Interface StatementKernel

Nested Class Summary

Method Summary

Methods inherited from interface components.standard.Standard

Method Details

kind

addToBlock

removeFromBlock

lengthOfBlock

assembleIf

disassembleIf

assembleIfElse

disassembleIfElse

assembleWhile

disassembleWhile

assembleCall

disassembleCall