Package components.program
Interface ProgramKernel
- All Known Subinterfaces:
Program
- All Known Implementing Classes:
Program1
,ProgramSecondary
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 TypeMethodDescriptionname()
Returns the name ofthis
.newBody()
Creates and returns aStatement
with a default initial value, of the dynamic type needed inswapBody
.Creates and returns an emptyMap<String, Statement>
of the dynamic type needed inswapContext
.void
Replaces the name ofthis
withn
.void
Exchanges the body ofthis
withb
;b
must have the dynamic type returned bynewBody
.void
Exchanges the context ofthis
withc
;c
must have the dynamic type returned bynewContext
.Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Method Details
-
name
Returns the name ofthis
.- Returns:
- the name of
this
- Ensures:
name = this.name
-
setName
Replaces the name ofthis
withn
.- Parameters:
n
- the name replacing the old one- Replaces:
this.name
- Requires:
[n is a valid IDENTIFIER]
- Ensures:
this.name = n
-
newContext
Creates and returns an emptyMap<String, Statement>
of the dynamic type needed inswapContext
.- Returns:
- a new empty
Map<String, Statement>
- Ensures:
newContext = {}
-
swapContext
Exchanges the context ofthis
withc
;c
must have the dynamic type returned bynewContext
.- Parameters:
c
- the context to be exchanged with that ofthis
- 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
Creates and returns aStatement
with a default initial value, of the dynamic type needed inswapBody
.- Returns:
- a new
Statement
- Ensures:
newBody = compose((BLOCK, ?, ?), <>)
-
swapBody
Exchanges the body ofthis
withb
;b
must have the dynamic type returned bynewBody
.- Parameters:
b
- the body to be exchanged with that ofthis
- Updates:
this.body, b
- Requires:
[b is a BLOCK statement]
- Ensures:
this.body = #b and b = #this.body
-