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.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
Modifier and Type | Method and Description |
---|---|
static Switch |
KeYJavaASTFactory.switchBlock(Expression expression,
Branch[] branches)
Create a switch block.
|
static Try |
KeYJavaASTFactory.tryBlock(StatementBlock body,
Branch[] branches)
Create a try block.
|
static Try |
KeYJavaASTFactory.tryBlock(Statement statement,
Branch branch)
Create a try block.
|
static Try |
KeYJavaASTFactory.tryBlock(Statement statement,
Branch[] branches)
Create a try block.
|
Modifier and Type | Class and Description |
---|---|
class |
BranchImp
Branch.
|
class |
Case
Case.
|
class |
Catch
Catch.
|
class |
Ccatch
Ccatch.
|
class |
Default
Default.
|
class |
Else
Else.
|
class |
Finally
Finally.
|
class |
Then
Then.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Branch> |
Switch.branches
Branches.
|
Modifier and Type | Method and Description |
---|---|
Branch |
Switch.getBranchAt(int index) |
Branch |
Exec.getBranchAt(int index)
Return the branch at the specified index in this node's "virtual" branch
array.
|
Branch |
Try.getBranchAt(int index)
Return the branch at the specified index in this node's
"virtual" branch array.
|
abstract Branch |
BranchStatement.getBranchAt(int index) |
Branch |
If.getBranchAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Branch> |
Switch.getBranchList() |
ImmutableArray<Branch> |
Exec.getBranchList()
Return the branch array wrapper
|
ImmutableArray<Branch> |
Try.getBranchList()
Return the branch array wrapper
|
Constructor and Description |
---|
Exec(StatementBlock body,
Branch[] branches)
Exec.
|
Switch(Expression e,
Branch[] branches)
Switch.
|
Try(StatementBlock body,
Branch[] branches)
Try.
|
Constructor and Description |
---|
Exec(StatementBlock body,
ImmutableArray<Branch> branches)
Exec.
|
Try(StatementBlock body,
ImmutableArray<Branch> branches)
Try.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Copyright © 2003-2019 The KeY-Project.