Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
Modifier and Type | Class and Description |
---|---|
class |
ContextStatementBlock
In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Method and Description |
---|---|
ProgramPrefix |
StatementBlock.getLastPrefixElement() |
ProgramPrefix |
StatementBlock.getNextPrefixElement() |
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<ProgramPrefix> |
StatementBlock.computePrefixElements(ImmutableArray<? extends Statement> b,
ProgramPrefix current)
computes the prefix elements for the given array of statment block
|
ImmutableArray<ProgramPrefix> |
StatementBlock.getPrefixElements() |
Modifier and Type | Method and Description |
---|---|
static ProgramPrefixUtil.ProgramPrefixInfo |
ProgramPrefixUtil.computeEssentials(ProgramPrefix prefix) |
static ImmutableArray<ProgramPrefix> |
StatementBlock.computePrefixElements(ImmutableArray<? extends Statement> b,
ProgramPrefix current)
computes the prefix elements for the given array of statment block
|
Modifier and Type | Class and Description |
---|---|
class |
Exec
Exec.
|
class |
LabeledStatement
Labeled statement.
|
class |
LoopScopeBlock
Loop scope block.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Try
Try.
|
Modifier and Type | Method and Description |
---|---|
ProgramPrefix |
Exec.getLastPrefixElement() |
ProgramPrefix |
LoopScopeBlock.getLastPrefixElement() |
ProgramPrefix |
MethodFrame.getLastPrefixElement() |
ProgramPrefix |
Try.getLastPrefixElement() |
ProgramPrefix |
SynchronizedBlock.getLastPrefixElement() |
ProgramPrefix |
LabeledStatement.getLastPrefixElement() |
ProgramPrefix |
Exec.getNextPrefixElement() |
ProgramPrefix |
LoopScopeBlock.getNextPrefixElement() |
ProgramPrefix |
MethodFrame.getNextPrefixElement() |
ProgramPrefix |
Try.getNextPrefixElement() |
ProgramPrefix |
SynchronizedBlock.getNextPrefixElement() |
ProgramPrefix |
LabeledStatement.getNextPrefixElement() |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<ProgramPrefix> |
Exec.getPrefixElements() |
ImmutableArray<ProgramPrefix> |
LoopScopeBlock.getPrefixElements() |
ImmutableArray<ProgramPrefix> |
MethodFrame.getPrefixElements() |
ImmutableArray<ProgramPrefix> |
Try.getPrefixElements() |
ImmutableArray<ProgramPrefix> |
SynchronizedBlock.getPrefixElements() |
ImmutableArray<ProgramPrefix> |
LabeledStatement.getPrefixElements() |
Modifier and Type | Method and Description |
---|---|
ProgramPrefix |
ProgramPrefix.getLastPrefixElement()
return the last prefix element
|
ProgramPrefix |
ProgramPrefix.getNextPrefixElement()
return the next prefix element
if no next prefix element is available an IndexOutOfBoundsException is thrown
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<ProgramPrefix> |
ProgramPrefix.getPrefixElements()
returns an array with all prefix elements starting at
this element
|
Copyright © 2003-2019 The KeY-Project.