KeYJavaASTFactory (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.java.KeYJavaASTFactory

Direct Known Subclasses:

CreateArrayMethodBuilder
```
public abstract class KeYJavaASTFactory
extends java.lang.Object
```
The KeYASTFactory helps building KeY Java AST structures.

Constructor Summary

Constructors
Constructor and Description

KeYJavaASTFactory()

Constructors
Constructor and Description
`KeYJavaASTFactory()`

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method and Description
`static ArrayReference`	`arrayFieldAccess(ReferencePrefix array, Expression index)` Create an array field access with a single index.
`static ArrayInitializer`	`arrayInitializer(Expression[] expressions, KeYJavaType type)` Create an array initializer.
`static FieldReference`	`arrayLength(JavaInfo model, ReferencePrefix array)` Create an array length access.
`static CopyAssignment`	`assign(Expression lhs, Expression rhs)` creates an assignment `lhs:=rhs`
`static CopyAssignment`	`assign(Expression lhs, Expression rhs, PositionInfo posInfo)` creates an assignment `lhs:=rhs`
`static CopyAssignment`	`assign(ExtList parameters)` Create an assignment.
`static CopyAssignment`	`assignArrayField(ProgramVariable variable, ReferencePrefix array, Expression index)` Create a statement that assigns an array element to a variable.
`static Expression`	`attribute(ReferencePrefix prefix, ProgramVariable field)` creates an attribute access `prefix.field`
`static StatementBlock`	`block(ExtList statements)` Create a block from an arbitrary number of statements.
`static StatementBlock`	`block(java.util.List<Statement> statements)` Create a block from an arbitrary number of statements.
`static StatementBlock`	`block(Statement... statements)` Create a block from an arbitrary number of statements.
`static Break`	`breakStatement(Label l)` Create a break statement.
`static Statement`	`breakStatement(Label label, PositionInfo positionInfo)`
`static Case`	`caseBlock(Expression expression, Statement statement)` Create a case block.
`static Case`	`caseBlock(Expression expression, Statement[] statements)` Create a case block.
`static Case`	`caseBlock(ExtList parameters, Expression expression, PositionInfo position)` Create a case block.
`static TypeCast`	`cast(Expression expression, KeYJavaType targetType)`
`static Catch`	`catchClause(ExtList parameters)` Create a catch clause.
`static Catch`	`catchClause(JavaInfo javaInfo, java.lang.String param, KeYJavaType kjt, StatementBlock body)` Create a catch clause.
`static Catch`	`catchClause(JavaInfo javaInfo, java.lang.String param, java.lang.String type, StatementBlock body)` Create a catch clause.
`static Catch`	`catchClause(ParameterDeclaration parameter, Statement[] statements)` Create a catch clause.
`static Catch`	`catchClause(ParameterDeclaration param, StatementBlock body)` create a catch clause
`static Continue`	`continueStatement(Label label)`
`static LocalVariableDeclaration`	`declare(ExtList parameters)` Create a local variable declaration without initialization.
`static LocalVariableDeclaration`	`declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, KeYJavaType type)` Create a local variable declaration with an arbitrary number of modifiers.
`static ProgramElement`	`declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, ProgramElementName typeName, int dimensions, ReferencePrefix typePrefix, KeYJavaType baseType)` Create a local array variable declaration with an arbitrary number of modifiers.
`static LocalVariableDeclaration`	`declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, TypeReference typeRef)` Create a local variable declaration with an arbitrary number of modifiers.
`static LocalVariableDeclaration`	`declare(ImmutableArray<Modifier> modifiers, TypeReference typeRef, VariableSpecification specification)` Create a local variable declaration.
`static LocalVariableDeclaration`	`declare(ImmutableArray<Modifier> modifiers, TypeReference typeRef, VariableSpecification[] specifications)` Create local variable declarations.
`static LocalVariableDeclaration`	`declare(IProgramVariable variable)` Create a local variable declaration without initialization.
`static LocalVariableDeclaration`	`declare(IProgramVariable variable, Expression init)` Create a local variable declaration.
`static LocalVariableDeclaration`	`declare(IProgramVariable var, Expression init, KeYJavaType type)` Create a local variable declaration.
`static LocalVariableDeclaration`	`declare(IProgramVariable var, KeYJavaType type)` Create a local variable declaration without initialization.
`static LocalVariableDeclaration`	`declare(Modifier[] modifiers, IProgramVariable variable, Expression init, KeYJavaType type)` Create a local variable declaration with an arbitrary number of modifiers.
`static LocalVariableDeclaration`	`declare(Modifier modifier, IProgramVariable variable, Expression init, KeYJavaType type)` Create a local variable declaration with a single modifier.
`static LocalVariableDeclaration`	`declare(ProgramElementName name, Expression init, KeYJavaType type)` create a local variable declaration `type name = init;`
`static LocalVariableDeclaration`	`declare(ProgramElementName name, KeYJavaType type)` Create a local variable declaration without initialization.
`static LocalVariableDeclaration`	`declare(ProgramElementName name, TypeReference typeRef)` creates a local variable declaration `typeRef name;`
`static LocalVariableDeclaration`	`declare(Services services, java.lang.String name, Expression initializer, KeYJavaType type)` Create a local variable declaration with a unique name.
`static LocalVariableDeclaration`	`declare(java.lang.String name, KeYJavaType type)` create a local variable declaration
`static LocalVariableDeclaration`	`declareMethodCall(IProgramVariable variable, ReferencePrefix reference, java.lang.String method)` Create a local variable declaration that assigns a method's return value initially.
`static LocalVariableDeclaration`	`declareMethodCall(KeYJavaType type, IProgramVariable variable, ReferencePrefix reference, java.lang.String method)` Create a local variable declaration that assigns a method's return value initially.
`static LocalVariableDeclaration`	`declareZero(KeYJavaType type, IProgramVariable variable)` Create a local variable declaration that assigns zero initially.
`static Default`	`defaultBlock(ExtList parameters)` Create a default block.
`static Default`	`defaultBlock(Statement statement)` Create a default block.
`static Default`	`defaultBlock(Statement[] statements)` Create a default block.
`static Do`	`doLoop(Expression condition, Statement statement, PositionInfo positionInfo)` Create a do loop.
`static Else`	`elseBlock(ExtList parameters)` Create an else block.
`static Else`	`elseBlock(Statement statement)` Create an else block.
`static Else`	`elseBlock(Statement[] statements)` Create an else block.
`static EmptyStatement`	`emptyStatement()` Create an empty statement.
`static EnhancedFor`	`enhancedForLoop(ExtList parameters)` Create an enhanced for loop.
`static Equals`	`equalsNullOperator(Expression expression)` Create an equality comparison with `null`.
`static Equals`	`equalsOperator(Expression left, Expression right)` Create an equals operator.
`static Equals`	`equalsOperator(ExtList operands)` Create an equals operator.
`static ExecutionContext`	`executionContext(KeYJavaType classType, IProgramMethod method, ReferencePrefix reference)` Create an execution context.
`static BooleanLiteral`	`falseLiteral()` Create a literal for the truth value `false`.
`static FieldReference`	`fieldReference(ReferencePrefix prefix, ProgramVariable field)` Create a field access.
`static FieldReference`	`fieldReference(Services services, java.lang.String name, Expression expression, ExecutionContext context)` Create a field access.
`static Finally`	`finallyBlock(ExtList parameters)` Create a finally block.
`static Finally`	`finallyBlock(Statement statement)` Create a finally block.
`static Finally`	`finallyBlock(Statement[] statements)` Create a finally block.
`static Finally`	`finallyBlock(StatementBlock body)` Create a finally block.
`static For`	`forLoop(ExtList parameters)` Create a for loop.
`static For`	`forLoop(IGuard guard, IForUpdates updates, Statement body)` Create a for loop with no initializer.
`static For`	`forLoop(IGuard guard, IForUpdates updates, Statement[] body)` Create a for loop with no initializer.
`static For`	`forLoop(ILoopInit init, IGuard guard, IForUpdates updates, Statement... statements)` Create a for loop from the loop definition and an arbitrary number of body statements.
`static IForUpdates`	`forUpdates(Expression update)` Create a list of loop updates that consists of a single expression.
`static Statement`	`ifElse(Expression guard, Statement thenStatement, Statement elseStatement)` Create an if clause.
`static If`	`ifElse(Expression guard, Then then, Else els)` Create an if statement including an else branch.
`static If`	`ifStatement(ExtList parameters)` Create an if statement.
`static If`	`ifThen(Expression guard, Statement... statements)` Create an if statement with no else branch.
`static If`	`ifThen(Expression guard, Statement then)` Create an if statement with no else branch.
`static If`	`ifThen(Expression guard, Then then)` Create an if statement with no else branch.
`static StatementBlock`	`insertStatementInBlock(Statement[] stmnt, StatementBlock b)` inserts the given statements at the begin of the block
`static StatementBlock`	`insertStatementInBlock(StatementBlock block, Statement[] statements)` Create a block where the given statements come after the given block.
`static StatementBlock`	`insertStatementInBlock(StatementBlock stmnt, StatementBlock b)` inserts the given statements at the begin of the block
`static StatementBlock`	`insertStatementInBlock(Statement statement, StatementBlock block)` Insert a statement in a block of statements.
`static Instanceof`	`instanceOf(Expression expression, KeYJavaType type)` Create an instance of operator.
`static IntLiteral`	`intLiteral(java.lang.Integer value)` Create an integer literal.
`static LabeledStatement`	`labeledStatement(ExtList parameters, Label label, PositionInfo position)` Create a labeled statement.
`static Statement`	`labeledStatement(Label label, Statement[] statements, PositionInfo pos)` Create a labeled block of statements.
`static LabeledStatement`	`labeledStatement(Label label, Statement statement, PositionInfo pos)` Create a labeled statement.
`static IGuard`	`lessThanArrayLengthGuard(JavaInfo model, ProgramVariable variable, ReferencePrefix array)` Create a condition that compares a variable and an array length using the less than operator.
`static IGuard`	`lessThanGuard(Expression left, Expression right)` Create a condition that compares two expressions using the less than operator.
`static LessThan`	`lessThanOperator(Expression left, Expression right)` Create a less than operator.
`static LessThan`	`lessThanZeroOperator(Expression expression)` Create a less than zero operator.
`static ProgramVariable`	`localVariable(ProgramElementName name, KeYJavaType kjt)` create a local variable
`static ProgramVariable`	`localVariable(Services services, java.lang.String name, KeYJavaType type)` Create a local variable with a unique name.
`static ProgramVariable`	`localVariable(java.lang.String name, KeYJavaType kjt)` create a local variable
`static LogicalAnd`	`logicalAndOperator(Expression left, Expression right)` Create a logical and operator.
`static LogicalOr`	`logicalOrOperator(Expression left, Expression right)` Create a logical or operator.
`static ILoopInit`	`loopInit(LoopInitializer init)` Create a loop initialization that consists of a single statement.
`static ILoopInit`	`loopInitZero(KeYJavaType type, IProgramVariable variable)` Create a loop initialization that declares and assigns zero to a local variable.
`static MethodBodyStatement`	`methodBody(JavaInfo model, ProgramVariable result, ReferencePrefix reference, KeYJavaType classType, java.lang.String methodName, ProgramVariable[] arguments)` Create a method body shortcut.
`static MethodBodyStatement`	`methodBody(ProgramVariable result, ReferencePrefix reference, IProgramMethod method, Expression[] arguments)` Create a method body shortcut.
`static MethodBodyStatement`	`methodBody(ProgramVariable result, ReferencePrefix reference, IProgramMethod method, ImmutableArray<Expression> arguments)` Create a method body shortcut.
`static MethodReference`	`methodCall(KeYJavaType type, java.lang.String name)` Create a method call on a type with no arguments.
`static MethodReference`	`methodCall(KeYJavaType type, java.lang.String name, Expression... args)` Create a method call on a type.
`static MethodReference`	`methodCall(KeYJavaType type, java.lang.String name, ImmutableArray<? extends Expression> args)` Create a method call on a type.
`static MethodReference`	`methodCall(ReferencePrefix reference, MethodName name, Expression... args)` Create a method call.
`static MethodReference`	`methodCall(ReferencePrefix reference, MethodName name, ImmutableArray<? extends Expression> args)` Create a method call.
`static MethodReference`	`methodCall(ReferencePrefix reference, java.lang.String name)` Create a method call with no arguments.
`static MethodReference`	`methodCall(ReferencePrefix reference, java.lang.String name, Expression... args)` Create a method call.
`static MethodReference`	`methodCall(ReferencePrefix reference, java.lang.String name, ImmutableArray<? extends Expression> args)` Create a method call.
`static MethodFrame`	`methodFrame(IExecutionContext executionContext, StatementBlock block)` Create a method call substitution.
`static MethodFrame`	`methodFrame(IExecutionContext executionContext, StatementBlock block, PositionInfo position)` Create a method call substitution at a specific source position.
`static MethodFrame`	`methodFrame(IProgramVariable result, IExecutionContext executionContext, StatementBlock block)` Create a method call substitution with a return value assignment.
`static MethodFrame`	`methodFrame(IProgramVariable result, IExecutionContext executionContext, StatementBlock block, PositionInfo position)` Create a method call substitution with a return value assignment at a specific source position.
`static NewArray`	`newArray(TypeReference typeRef, int dimensions, ArrayInitializer initializer, KeYJavaType keyJavaType)` Create an array instantiation.
`static NewArray`	`newArray(TypeReference typeRef, int dimensions, Expression[] sizes, ArrayInitializer initializer, KeYJavaType keyJavaType)` Create an array instantiation.
`static NewArray`	`newArray(TypeReference typeRef, int dimensions, Expression[] sizes, KeYJavaType keyJavaType)` Create an array instantiation.
`static NewArray`	`newArray(TypeReference typeRef, int dimensions, Expression size, KeYJavaType keyJavaType)` Create an array instantiation.
`static New`	`newOperator(KeYJavaType type)` Create an object allocation without arguments.
`static New`	`newOperator(ReferencePrefix referencePrefix, KeYJavaType type)` Create an object allocation without arguments.
`static New`	`newOperator(ReferencePrefix referencePrefix, KeYJavaType type, Expression[] args)` Create an object allocation.
`static New`	`newOperator(ReferencePrefix referencePrefix, TypeReference typeReference, Expression[] args)` Create an object allocation.
`static NotEquals`	`notEqualsOperator(ExtList operands)` Create an unequal operator.
`static ParameterDeclaration`	`parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, IProgramVariable var)` Create a parameter declaration.
`static ParameterDeclaration`	`parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, java.lang.String name)` create a parameter declaration
`static ParameterDeclaration`	`parameterDeclaration(JavaInfo javaInfo, java.lang.String type, java.lang.String name)`
`static ParenthesizedExpression`	`parenthesizedExpression(Expression expression)` Create a parenthesized expression.
`static PassiveExpression`	`passiveExpression(Expression expression)` Create an inactive expression.
`static IForUpdates`	`postIncrementForUpdates(ProgramVariable variable)` Create a loop update expression that post increments a given variable.
`static Return`	`returnClause(Expression e)` Create a return clause.
`static SuperConstructorReference`	`superConstructor(ReferencePrefix referencePrefix, Expression[] args)` Create a call to the super constructor.
`static SuperReference`	`superReference()` Create a reference to `super`.
`static Switch`	`switchBlock(Expression expression, Branch[] branches)` Create a switch block.
`static Switch`	`switchBlock(ExtList parameters)` Create a switch block.
`static SynchronizedBlock`	`synchronizedBlock(ExtList parameters)` Create a synchronized block.
`static Then`	`thenBlock(ExtList parameters)` Create a then block.
`static Then`	`thenBlock(Statement statement)` Create a then block.
`static Then`	`thenBlock(Statement[] statements)` Create a then block.
`static ThisConstructorReference`	`thisConstructor(Expression[] args)` Create a call to a constructor of the current class.
`static ThisReference`	`thisReference()` Create a reference to `this`.
`static Throw`	`throwClause(Expression e)` Create a throw clause.
`static TransactionStatement`	`transactionStatement(int type)` Create a transaction statement.
`static Guard`	`trueGuard()` Create a `true` condition.
`static BooleanLiteral`	`trueLiteral()` Create a literal for the truth value `true`.
`static Try`	`tryBlock(ExtList parameters)` Create a try block.
`static Try`	`tryBlock(StatementBlock body, Branch[] branches)` Create a try block.
`static Try`	`tryBlock(Statement statement, Branch branch)` Create a try block.
`static Try`	`tryBlock(Statement statement, Branch[] branches)` Create a try block.
`static TypeRef`	`typeRef(KeYJavaType type)` Create a type reference.
`static TypeRef`	`typeRef(KeYJavaType type, int dimensions)` Create a type reference.
`static VariableSpecification`	`variableSpecification(IProgramVariable variable, Expression initializer, KeYJavaType keyJavaType)` Create a variable specification.
`static VariableSpecification`	`variableSpecification(IProgramVariable variable, int dimensions, Expression initializer, Type type)` Create a variable specification.
`static Statement`	`whileLoop(Expression condition, Statement body)` Create a while loop.
`static While`	`whileLoop(Expression condition, Statement body, PositionInfo position)` Create a while loop at a specific source position.
`static IntLiteral`	`zeroLiteral()` Create a literal for the integer zero.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Constructor Detail
  - KeYJavaASTFactory
```
public KeYJavaASTFactory()
```
- Method Detail
  - assign
```
public static CopyAssignment assign(Expression lhs,
                                    Expression rhs)
```
    creates an assignment lhs:=rhs
  - assign
```
public static CopyAssignment assign(Expression lhs,
                                    Expression rhs,
                                    PositionInfo posInfo)
```
    creates an assignment lhs:=rhs
  - assign
```
public static CopyAssignment assign(ExtList parameters)
```
    Create an assignment.
    
    Parameters:
    
    parameters - the assignment parameters (variable, expression) as ExtList
    
    Returns:
    
    a new CopyAssignment as defined by parameters
  - attribute
```
public static Expression attribute(ReferencePrefix prefix,
                                   ProgramVariable field)
```
    creates an attribute access prefix.field
  - declare
```
public static LocalVariableDeclaration declare(ProgramElementName name,
                                               TypeReference typeRef)
```
    creates a local variable declaration typeRef name;
  - declare
```
public static LocalVariableDeclaration declare(ProgramElementName name,
                                               KeYJavaType type)
```
    Create a local variable declaration without initialization.
```
 type name;
 
```
    Parameters:
    
    name - the ProgramElementName of the variable to be declared
    
    type - the static KeYJavaType of the variable to be declared
    
    Returns:
    
    a new LocalVariableDeclaration of a variable with static type type and name name
  - declare
```
public static LocalVariableDeclaration declare(ProgramElementName name,
                                               Expression init,
                                               KeYJavaType type)
```
    create a local variable declaration
    
    type name = init;
  - declare
```
public static LocalVariableDeclaration declare(IProgramVariable var,
                                               Expression init,
                                               KeYJavaType type)
```
    Create a local variable declaration.
```
 type var = init;
 
```
    Parameters:
    
    var - the named and typed IProgramVariable to be declared
    
    init - the Expression var is initialized with
    
    type - the static KeYJavaType of var
    
    Returns:
    
    a LocalVariableDeclaration of var with static type type and initial value init
  - declare
```
public static LocalVariableDeclaration declare(Services services,
                                               java.lang.String name,
                                               Expression initializer,
                                               KeYJavaType type)
```
    Create a local variable declaration with a unique name.
```
 type name{unique} = initializer;
 
```
    Parameters:
    
    services - the Services whose VariableNamer is used to determine a unique variable name
    
    name - the String on which the variable's unique name is based
    
    initializer - the Expression the declared variable is initialized with
    
    type - the static KeYJavaType of the to be declared variable
    
    Returns:
    
    a LocalVariableDeclaration of variable named uniquely after name with static type type and initial value initializer
  - declare
```
public static LocalVariableDeclaration declare(IProgramVariable var,
                                               KeYJavaType type)
```
    Create a local variable declaration without initialization.
```
 type var;
 
```
    Parameters:
    
    var - the named and typed IProgramVariable to be declared
    
    type - the static KeYJavaType of var
    
    Returns:
    
    a LocalVariableDeclaration of var with static type type
  - declare
```
public static LocalVariableDeclaration declare(java.lang.String name,
                                               KeYJavaType type)
```
    create a local variable declaration
  - parameterDeclaration
```
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo,
                                                        KeYJavaType kjt,
                                                        java.lang.String name)
```
    create a parameter declaration
  - parameterDeclaration
```
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo,
                                                        KeYJavaType kjt,
                                                        IProgramVariable var)
```
    Create a parameter declaration.
```
 kjt var
 
```
    Parameters:
    
    javaInfo - the Java model containing kjt
    
    kjt - the static KeYJavaType of var
    
    var - the named and typed IProgramVariable to be declared as parameter
    
    Returns:
    
    a ParameterDeclaration of var with static type kjt
  - parameterDeclaration
```
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo,
                                                        java.lang.String type,
                                                        java.lang.String name)
```
  - parenthesizedExpression
```
public static ParenthesizedExpression parenthesizedExpression(Expression expression)
```
    Create a parenthesized expression.
```
 (expression)
 
```
    Parameters:
    
    expression - the Expression to be parenthesized
    
    Returns:
    
    a new ParenthesizedExpression of expression
  - passiveExpression
```
public static PassiveExpression passiveExpression(Expression expression)
```
    Create an inactive expression.
    
    Parameters:
    
    expression - the Expression to be marked inactive
    
    Returns:
    
    a new PassiveExpression version of expression
  - localVariable
```
public static ProgramVariable localVariable(java.lang.String name,
                                            KeYJavaType kjt)
```
    create a local variable
  - localVariable
```
public static ProgramVariable localVariable(ProgramElementName name,
                                            KeYJavaType kjt)
```
    create a local variable
  - localVariable
```
public static ProgramVariable localVariable(Services services,
                                            java.lang.String name,
                                            KeYJavaType type)
```
    Create a local variable with a unique name.
    
    Parameters:
    
    services - the Services whose VariableNamer is used
    
    name - the String on which the variable's unique name is based
    
    type - the variable's static KeYJavaType
    
    Returns:
    
    a new ProgramVariable of static type type and with a unique name based on name
  - logicalAndOperator
```
public static LogicalAnd logicalAndOperator(Expression left,
                                            Expression right)
```
    Create a logical and operator.
```
 left & right
 
```
    Parameters:
    
    left - the left operand Expression
    
    right - the right operand Expression
    
    Returns:
    
    a new LogicalAnd of left and right
  - logicalOrOperator
```
public static LogicalOr logicalOrOperator(Expression left,
                                          Expression right)
```
    Create a logical or operator.
```
 left | right
 
```
    Parameters:
    
    left - the left operand Expression
    
    right - the right operand Expression
    
    Returns:
    
    a new LogicalOr of left and right
  - catchClause
```
public static Catch catchClause(ExtList parameters)
```
    Create a catch clause.
    
    Parameters:
    
    parameters - the catch clause parameters (exception, body) as ExtList
    
    Returns:
    
    a new Catch as defined by parameters
  - catchClause
```
public static Catch catchClause(ParameterDeclaration param,
                                StatementBlock body)
```
    create a catch clause
  - catchClause
```
public static Catch catchClause(ParameterDeclaration parameter,
                                Statement[] statements)
```
    Create a catch clause.
```
 catch (parameter) {
     statements
 }
 
```
    Parameters:
    
    parameter - the to be caught ParameterDeclaration
    
    statements - the body Statements
    
    Returns:
    
    a new Catch clause for execution of statements in case of parameter
  - catchClause
```
public static Catch catchClause(JavaInfo javaInfo,
                                java.lang.String param,
                                KeYJavaType kjt,
                                StatementBlock body)
```
    Create a catch clause.
```
 catch (kjt param)
    body
 
```
    Parameters:
    
    javaInfo - the JavaInfo containing kjt
    
    param - the String name of the exception object variable
    
    kjt - the KeYJavaType of the exception object variable
    
    body - the StatementBlock catch clause body
    
    Returns:
    
    a new Catch with parameter param of static type kjt and body body
  - catchClause
```
public static Catch catchClause(JavaInfo javaInfo,
                                java.lang.String param,
                                java.lang.String type,
                                StatementBlock body)
```
    Create a catch clause.
```
 catch (type param)
    body
 
```
    Parameters:
    
    javaInfo - the JavaInfo containing a KeYJavaType named type
    
    param - the String name of the exception object variable
    
    type - the String name of the exception object variable's KeYJavaType
    
    body - the StatementBlock catch clause body
    
    Returns:
    
    a new Catch with parameter param of static type type and body body
  - throwClause
```
public static Throw throwClause(Expression e)
```
    Create a throw clause.
```
 throw e
 
```
    Parameters:
    
    e - the throw Expression
    
    Returns:
    
    a new Throw statement with expression e
  - transactionStatement
```
public static TransactionStatement transactionStatement(int type)
```
    Create a transaction statement.
    
    Parameters:
    
    type - the transaction statement type
    
    Returns:
    
    a new TransactionStatement of type type
  - trueGuard
```
public static Guard trueGuard()
```
    Create a true condition.
    
    Returns:
    
    a new Guard with expression true
  - whileLoop
```
public static Statement whileLoop(Expression condition,
                                  Statement body)
```
    Create a while loop.
```
 while (condition)
     body
 
```
    Parameters:
    
    condition - the loop condition Expression
    
    body - the loop body Statement
    
    Returns:
    
    a new While loop defined by condition and body
  - whileLoop
```
public static While whileLoop(Expression condition,
                              Statement body,
                              PositionInfo position)
```
    Create a while loop at a specific source position.
```
 while (condition)
     body
 
```
    Parameters:
    
    condition - the loop condition Expression
    
    body - the loop body Statement
    
    position - the new source element's PositionInfo
    
    Returns:
    
    a new While loop defined by condition and body, and positioned at position
  - returnClause
```
public static Return returnClause(Expression e)
```
    Create a return clause.
```
 return e
 
```
    Parameters:
    
    e - the return Expression
    
    Returns:
    
    a new Return statement with expression e
  - ifThen
```
public static If ifThen(Expression guard,
                        Statement then)
```
    Create an if statement with no else branch.
```
 if (guard)
    then
 
```
    Parameters:
    
    guard - the if statement condition Expression
    
    then - the if statement then branch Statement
    
    Returns:
    
    an If with expression guard and then branch then
  - ifThen
```
public static If ifThen(Expression guard,
                        Statement... statements)
```
    Create an if statement with no else branch.
```
 if (guard) {
    statements
 }
 
```
    Parameters:
    
    guard - the if statement condition Expression
    
    statements - the if statement then branch Statements
    
    Returns:
    
    an If with condition guard and then branch statements
  - ifThen
```
public static If ifThen(Expression guard,
                        Then then)
```
    Create an if statement with no else branch.
```
 if (guard)
    then
 
```
    Parameters:
    
    guard - the if statement condition Expression
    
    then - the if statement then branch Then
    
    Returns:
    
    an If with expression guard and then branch then
  - ifStatement
```
public static If ifStatement(ExtList parameters)
```
    Create an if statement.
    
    Parameters:
    
    parameters - the if statement parameters (guard, body, else branch) as ExtList
    
    Returns:
    
    a new If as defined by parameters
  - ifElse
```
public static If ifElse(Expression guard,
                        Then then,
                        Else els)
```
    Create an if statement including an else branch.
```
 if (guard)
    then
 else
    els
 
```
    Parameters:
    
    guard - the if statement condition Expression
    
    then - the if statement then branch Statement
    
    els - the if statement else branch Statement
    
    Returns:
    
    an If with expression guard, then branch then and else branch els
  - ifElse
```
public static Statement ifElse(Expression guard,
                               Statement thenStatement,
                               Statement elseStatement)
```
    Create an if clause.
```
 if (guard)
    thenStatement
 else
    elseStatement
 
```
    Parameters:
    
    guard - the if clause condition Expression
    
    thenStatement - the if clause then branch Statement
    
    elseStatement - the if clause else branch Statement
    
    Returns:
    
    a new If with condition guard, then branch thenStatement and else branch elseStatement
  - breakStatement
```
public static Break breakStatement(Label l)
```
    Create a break statement.
    
    Parameters:
    
    l - the break destination Label
    
    Returns:
    
    a new Break with label l
  - breakStatement
```
public static Statement breakStatement(Label label,
                                       PositionInfo positionInfo)
```
  - caseBlock
```
public static Case caseBlock(ExtList parameters,
                             Expression expression,
                             PositionInfo position)
```
    Create a case block.
    
    Parameters:
    
    parameters - the case block parameters (body) as ExtList
    
    expression - the case block Expression
    
    position - the new source element's PositionInfo
    
    Returns:
    
    a new Case as defined by parameters and expression
  - caseBlock
```
public static Case caseBlock(Expression expression,
                             Statement statement)
```
    Create a case block.
```
 case (expression)
     statement
 
```
    Parameters:
    
    expression - the case Expression
    
    statement - the to be executed Statement
    
    Returns:
    
    a new Case for execution of statement in case of expression
  - caseBlock
```
public static Case caseBlock(Expression expression,
                             Statement[] statements)
```
    Create a case block.
```
 case (expression) {
     statements
 }
 
```
    Parameters:
    
    expression - the case Expression
    
    statements - the to be executed Statements
    
    Returns:
    
    a new Case for execution of statements in case of expression
  - continueStatement
```
public static Continue continueStatement(Label label)
```
  - emptyStatement
```
public static EmptyStatement emptyStatement()
```
    Create an empty statement.
    
    Returns:
    
    a new EmptyStatement
  - enhancedForLoop
```
public static EnhancedFor enhancedForLoop(ExtList parameters)
```
    Create an enhanced for loop.
    
    Parameters:
    
    parameters - the loop definition parameters (initializer, guard, body) as ExtList
    
    Returns:
    
    a new For as defined by parameters
  - equalsNullOperator
```
public static Equals equalsNullOperator(Expression expression)
```
    Create an equality comparison with null.
```
 expression == null
 
```
    Parameters:
    
    expression - the Expression to be compared against null
    
    Returns:
    
    a new Equals that compares expression against null
  - equalsOperator
```
public static Equals equalsOperator(Expression left,
                                    Expression right)
```
    Create an equals operator.
```
 left == right
 
```
    Parameters:
    
    left - the left operand Expression
    
    right - the right operand Expression
    
    Returns:
    
    a new Equals of left and right
  - equalsOperator
```
public static Equals equalsOperator(ExtList operands)
```
    Create an equals operator.
```
 operand{1} == operand{2}
 
```
    Parameters:
    
    operands - the operands ExtList
    
    Returns:
    
    a new Equals of operands
  - executionContext
```
public static ExecutionContext executionContext(KeYJavaType classType,
                                                IProgramMethod method,
                                                ReferencePrefix reference)
```
    Create an execution context.
    
    Parameters:
    
    classType - the enclosing class KeYJavaType
    
    method - the enclosing IProgramMethod defined in classType
    
    reference - the ReferencePrefix method is called on
    
    Returns:
    
    a new ExecutionContext for calls on reference to method from classType
  - insertStatementInBlock
```
public static StatementBlock insertStatementInBlock(Statement statement,
                                                    StatementBlock block)
```
    Insert a statement in a block of statements.
    
    Parameters:
    
    statement - the Statement to be inserted into block
    
    block - the StatementBlock statement is inserted into
    
    Returns:
    
    a new StatementBlock that contains both the Statements from block and statement
  - insertStatementInBlock
```
public static StatementBlock insertStatementInBlock(Statement[] stmnt,
                                                    StatementBlock b)
```
    inserts the given statements at the begin of the block
    
    Parameters:
    
    stmnt - array of Statement those have to be inserted
    
    b - the Statementblock where to insert
  - insertStatementInBlock
```
public static StatementBlock insertStatementInBlock(StatementBlock stmnt,
                                                    StatementBlock b)
```
    inserts the given statements at the begin of the block
    
    Parameters:
    
    stmnt - array of Statement those have to be inserted
    
    b - the Statementblock where to insert
  - insertStatementInBlock
```
public static StatementBlock insertStatementInBlock(StatementBlock block,
                                                    Statement[] statements)
```
    Create a block where the given statements come after the given block.
```
 block
 statements
 
```
    Parameters:
    
    block - the original StatementBlock
    
    statements - the inserted Statements
    
    Returns:
    
    a new StatementBlock that contains block first and statements second
  - instanceOf
```
public static Instanceof instanceOf(Expression expression,
                                    KeYJavaType type)
```
    Create an instance of operator.
```
 expression instance of type
 
```
    Parameters:
    
    expression - the Expression operand, whose runtime type is to be checked
    
    type - the KeYJavaType operand expression's type is checked against
    
    Returns:
    
    a new Instanceof for checking expression's type against type
  - declareZero
```
public static LocalVariableDeclaration declareZero(KeYJavaType type,
                                                   IProgramVariable variable)
```
    Create a local variable declaration that assigns zero initially.
```
 type variable = 0;
 
```
    Parameters:
    
    type - the static KeYJavaType of variable
    
    variable - the named and typed IProgramVariable to be declared
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value zero
  - declareMethodCall
```
public static LocalVariableDeclaration declareMethodCall(KeYJavaType type,
                                                         IProgramVariable variable,
                                                         ReferencePrefix reference,
                                                         java.lang.String method)
```
    Create a local variable declaration that assigns a method's return value initially.
```
 type variable = reference.method();
 
```
    Parameters:
    
    type - the static KeYJavaType of variable
    
    variable - the named and typed IProgramVariable to be declared
    
    reference - the ReferencePrefix the method is called on
    
    method - the method's name String
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value reference.method()
  - declareMethodCall
```
public static LocalVariableDeclaration declareMethodCall(IProgramVariable variable,
                                                         ReferencePrefix reference,
                                                         java.lang.String method)
```
    Create a local variable declaration that assigns a method's return value initially.
```
 type variable = reference.method();
 
```
    where type is variable's KeYJavaType as it is returned by IProgramVariable.getKeYJavaType().
    Parameters:
    
    variable - the named and typed IProgramVariable to be declared
    
    reference - the ReferencePrefix the method is called on
    
    method - the method's name String
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value reference.method()
  - defaultBlock
```
public static Default defaultBlock(ExtList parameters)
```
    Create a default block.
    
    Parameters:
    
    parameters - the default block parameters (body) as ExtList
    
    Returns:
    
    a new Default as defined by parameters
  - defaultBlock
```
public static Default defaultBlock(Statement statement)
```
    Create a default block.
```
 default
     statement
 
```
    Parameters:
    
    statement - the to be executed Statement
    
    Returns:
    
    a new Default that contains statement
  - defaultBlock
```
public static Default defaultBlock(Statement[] statements)
```
    Create a default block.
```
 default {
     statements
 }
 
```
    Parameters:
    
    statements - the to be executed Statements
    
    Returns:
    
    a new Default that contains statements
  - doLoop
```
public static Do doLoop(Expression condition,
                        Statement statement,
                        PositionInfo positionInfo)
```
    Create a do loop.
```
 do
     statement
 while (condition);
 
```
    Parameters:
    
    condition - the do-loop condition Expression
    
    statement - the do-loop body Statement
    
    positionInfo - the new source element's PositionInfo
    
    Returns:
    
    a new Do that executes statement while condition holds
  - elseBlock
```
public static Else elseBlock(ExtList parameters)
```
    Create an else block.
    
    Parameters:
    
    parameters - the else block parameters (body) as ExtList
    
    Returns:
    
    a new Else as defined by parameters
  - elseBlock
```
public static Else elseBlock(Statement statement)
```
    Create an else block.
```
 else
     statement
 
```
    Parameters:
    
    statement - the Statement to be executed
    
    Returns:
    
    a new Else block consisting of statement solely
  - elseBlock
```
public static Else elseBlock(Statement[] statements)
```
    Create an else block.
```
 else {
     statements
 }
 
```
    Parameters:
    
    statements - the Statements to be executed
    
    Returns:
    
    a new Else block consisting of statements solely
  - loopInit
```
public static ILoopInit loopInit(LoopInitializer init)
```
    Create a loop initialization that consists of a single statement.
```
 init
 
```
    Parameters:
    
    init - the single LoopInitializer
    
    Returns:
    
    a new ILoopInit that consists of init only
  - loopInitZero
```
public static ILoopInit loopInitZero(KeYJavaType type,
                                     IProgramVariable variable)
```
    Create a loop initialization that declares and assigns zero to a local variable.
```
 type variable = 0
 
```
    Parameters:
    
    type - the static KeYJavaType of variable
    
    variable - the named and typed IProgramVariable to be declared
    
    Returns:
    
    a new ILoopInit that declares variable variable with static type type and initial value zero
  - arrayInitializer
```
public static ArrayInitializer arrayInitializer(Expression[] expressions,
                                                KeYJavaType type)
```
    Create an array initializer.
    
    Parameters:
    
    expressions - the initial value Expressions
    
    type - the array type KeYJavaType
    
    Returns:
    
    a new ArrayInitializer which contains expressions and is of type type
  - arrayLength
```
public static FieldReference arrayLength(JavaInfo model,
                                         ReferencePrefix array)
```
    Create an array length access.
```
 array.length
 
```
    Parameters:
    
    model - the JavaInfo to retrieve the array super class type, which holds the length attribute, from
    
    array - the ReferencePrefix whose length attribute is accessed
    
    Returns:
    
    a new FieldReference for array's length attribute
  - lessThanGuard
```
public static IGuard lessThanGuard(Expression left,
                                   Expression right)
```
    Create a condition that compares two expressions using the less than operator.
```
 left < right
 
```
    Parameters:
    
    left - the Expression to be compared less than right
    
    right - the Expression to be compared greater than left
    
    Returns:
    
    a new Guard that compares left less than right
  - lessThanOperator
```
public static LessThan lessThanOperator(Expression left,
                                        Expression right)
```
    Create a less than operator.
```
 left < right
 
```
    Parameters:
    
    left - the left operand Expression
    
    right - the right operand Expression
    
    Returns:
    
    a new LessThan that compares left less than right
  - lessThanZeroOperator
```
public static LessThan lessThanZeroOperator(Expression expression)
```
    Create a less than zero operator.
```
 expression < 0
 
```
    Parameters:
    
    expression - the left operand Expression
    
    Returns:
    
    a new LessThan that compares expression less than 0
  - lessThanArrayLengthGuard
```
public static IGuard lessThanArrayLengthGuard(JavaInfo model,
                                              ProgramVariable variable,
                                              ReferencePrefix array)
```
    Create a condition that compares a variable and an array length using the less than operator.
```
 variable < array.length
 
```
    Parameters:
    
    model - the JavaInfo to retrieve the array super class type, which holds the length attribute, from
    
    variable - the ProgramVariable to be compared less than array's length
    
    array - the ReferencePrefix whose length attribute is accessed
    
    Returns:
    
    a new Guard that compares variable less than array's length
  - forUpdates
```
public static IForUpdates forUpdates(Expression update)
```
    Create a list of loop updates that consists of a single expression.
```
 update
 
```
    Parameters:
    
    update - the single update Expression
    
    Returns:
    
    a new ForUpdates that consists of update only
  - postIncrementForUpdates
```
public static IForUpdates postIncrementForUpdates(ProgramVariable variable)
```
    Create a loop update expression that post increments a given variable.
```
 variable++
 
```
    Parameters:
    
    variable - the ProgramVariable to be post incremented during the loop updates
    
    Returns:
    
    a new ForUpdates that consists of the post increment of variable
  - arrayFieldAccess
```
public static ArrayReference arrayFieldAccess(ReferencePrefix array,
                                              Expression index)
```
    Create an array field access with a single index.
```
 array[index]
 
```
    Parameters:
    
    array - the ReferencePrefix to be accessed
    
    index - the array access index Expression
    
    Returns:
    
    a new ArrayReference for access of array at index
  - block
```
public static StatementBlock block(ExtList statements)
```
    Create a block from an arbitrary number of statements.
    
    Parameters:
    
    statements - the block statements as ExtList
    
    Returns:
    
    a new StatementBlock consisting of statements
  - block
```
public static StatementBlock block(Statement... statements)
```
    Create a block from an arbitrary number of statements.
```
 {
   statements;
 }
 
```
    Parameters:
    
    statements - the Statements to appear in the block
    
    Returns:
    
    a new StatementBlock that consists of the given statements in the very same order
  - block
```
public static StatementBlock block(java.util.List<Statement> statements)
```
    Create a block from an arbitrary number of statements.
```
 {
   statements;
 }
 
```
    Parameters:
    
    statements - the Statements to appear in the block
    
    Returns:
    
    a new StatementBlock that consists of the given statements in the very same order
  - forLoop
```
public static For forLoop(ExtList parameters)
```
    Create a for loop.
    
    Parameters:
    
    parameters - the loop definition parameters (initializer, guard, updates, body) as ExtList
    
    Returns:
    
    a new For as defined by parameters
  - forLoop
```
public static For forLoop(ILoopInit init,
                          IGuard guard,
                          IForUpdates updates,
                          Statement... statements)
```
    Create a for loop from the loop definition and an arbitrary number of body statements.
```
 for (init; guard; updates) {
    statements;
 }
 
```
    Parameters:
    
    init - the ILoopInit loop initializations
    
    guard - the IGuard loop condition
    
    updates - the IForUpdates loop updates
    
    statements - the body Statements
    
    Returns:
    
    a new For with initializers init, condition guard, updates updates and body statements
  - forLoop
```
public static For forLoop(IGuard guard,
                          IForUpdates updates,
                          Statement body)
```
    Create a for loop with no initializer.
```
 for (; guard; updates)
     body
 
```
    Parameters:
    
    guard - the IGuard loop condition
    
    updates - the IForUpdates loop updates
    
    body - the body Statement
    
    Returns:
    
    a new For with condition guard, updates updates and body body
  - forLoop
```
public static For forLoop(IGuard guard,
                          IForUpdates updates,
                          Statement[] body)
```
    Create a for loop with no initializer.
```
 for (; guard; updates)
     body
 
```
    Parameters:
    
    guard - the IGuard loop condition
    
    updates - the IForUpdates loop updates
    
    body - the body Statements
    
    Returns:
    
    a new For with condition guard, updates updates and body body
  - assignArrayField
```
public static CopyAssignment assignArrayField(ProgramVariable variable,
                                              ReferencePrefix array,
                                              Expression index)
```
    Create a statement that assigns an array element to a variable.
```
 variable = array[index];
 
```
    Parameters:
    
    variable - the ProgramVariable to be assigned to
    
    array - the array ReferencePrefix to be accessed
    
    index - the array access index Expression
    
    Returns:
    
    a new CopyAssignment of array element at index to variable
  - declare
```
public static LocalVariableDeclaration declare(ExtList parameters)
```
    Create a local variable declaration without initialization.
    
    Parameters:
    
    parameters - the declaration parameters (modifiers, type reference, variable specifications) as ExtList
    
    Returns:
    
    a new LocalVariableDeclaration as defined by parameters
  - declare
```
public static LocalVariableDeclaration declare(IProgramVariable variable)
```
    Create a local variable declaration without initialization.
```
 type variable;
 
```
    where type is variable's KeYJavaType as it is returned by IProgramVariable.getKeYJavaType().
    Parameters:
    
    variable - the named and typed IProgramVariable to be declared
    
    Returns:
    
    a new LocalVariableDeclaration of variable
  - declare
```
public static LocalVariableDeclaration declare(IProgramVariable variable,
                                               Expression init)
```
    Create a local variable declaration.
```
 type variable = init;
 
```
    where type is variable's KeYJavaType as it is returned by IProgramVariable.getKeYJavaType().
    Parameters:
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    Returns:
    
    a new LocalVariableDeclaration of variable
  - declare
```
public static LocalVariableDeclaration declare(Modifier modifier,
                                               IProgramVariable variable,
                                               Expression init,
                                               KeYJavaType type)
```
    Create a local variable declaration with a single modifier.
```
 modifier type variable = init;
 
```
    Parameters:
    
    modifier - the Modifier
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    type - the static KeYJavaType of variable
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value init
  - declare
```
public static LocalVariableDeclaration declare(Modifier[] modifiers,
                                               IProgramVariable variable,
                                               Expression init,
                                               KeYJavaType type)
```
    Create a local variable declaration with an arbitrary number of modifiers.
```
 modifiers type variable = init;
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    type - the static KeYJavaType of variable
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value init
  - declare
```
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers,
                                               IProgramVariable variable,
                                               Expression init,
                                               KeYJavaType type)
```
    Create a local variable declaration with an arbitrary number of modifiers.
```
 modifiers type variable = init;
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    type - the static KeYJavaType of variable
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type type and initial value init
  - declare
```
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers,
                                               IProgramVariable variable,
                                               Expression init,
                                               TypeReference typeRef)
```
    Create a local variable declaration with an arbitrary number of modifiers.
```
 modifiers typeRef variable = init;
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    typeRef - the static TypeRef of variable
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type typeRef and initial value init
  - declare
```
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers,
                                               TypeReference typeRef,
                                               VariableSpecification specification)
```
    Create a local variable declaration.
```
 modifiers typeRef specification
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    typeRef - the static TypeRef of the variable to be declared
    
    specification - the VariableSpecification of the variable to be declared
    
    Returns:
    
    a new LocalVariableDeclaration of the variable specified by specification with static type typeRef
  - declare
```
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers,
                                               TypeReference typeRef,
                                               VariableSpecification[] specifications)
```
    Create local variable declarations.
```
 modifiers typeRef specification{1}, ...
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    typeRef - the static TypeRef of the variable to be declared
    
    specifications - the VariableSpecifications of the variables to be declared
    
    Returns:
    
    a new LocalVariableDeclaration of the variables specified by specifications with static type typeRef
  - methodCall
```
public static MethodReference methodCall(ReferencePrefix reference,
                                         java.lang.String name,
                                         ImmutableArray<? extends Expression> args)
```
    Create a method call.
```
 reference.name(args);
 
```
    Parameters:
    
    reference - the ReferencePrefix the method is called on
    
    name - the method's name String
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on reference with arguments args
  - methodCall
```
public static MethodReference methodCall(KeYJavaType type,
                                         java.lang.String name,
                                         ImmutableArray<? extends Expression> args)
```
    Create a method call on a type.
```
 type.name(args);
 
```
    Parameters:
    
    type - the KeYJavaType the method is called on
    
    name - the method's name String
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on type with arguments args
  - methodCall
```
public static MethodReference methodCall(KeYJavaType type,
                                         java.lang.String name,
                                         Expression... args)
```
    Create a method call on a type.
```
 type.name(args);
 
```
    Parameters:
    
    type - the KeYJavaType the method is called on
    
    name - the method's name String
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on type with arguments args
  - methodCall
```
public static MethodReference methodCall(KeYJavaType type,
                                         java.lang.String name)
```
    Create a method call on a type with no arguments.
```
 type.name();
 
```
    Parameters:
    
    type - the KeYJavaType the method is called on
    
    name - the method's name String
    
    Returns:
    
    a new MethodReference for call of method name on type with arguments args
  - methodCall
```
public static MethodReference methodCall(ReferencePrefix reference,
                                         java.lang.String name)
```
    Create a method call with no arguments.
```
 reference.name();
 
```
    Parameters:
    
    reference - the ReferencePrefix the method is called on
    
    name - the method's name String
    
    Returns:
    
    a new MethodReference for call of method name on reference with no arguments
  - methodCall
```
public static MethodReference methodCall(ReferencePrefix reference,
                                         java.lang.String name,
                                         Expression... args)
```
    Create a method call.
```
 reference.name(args);
 
```
    Parameters:
    
    reference - the ReferencePrefix the method is called on
    
    name - the method's name String
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on reference with arguments args
  - methodCall
```
public static MethodReference methodCall(ReferencePrefix reference,
                                         MethodName name,
                                         Expression... args)
```
    Create a method call.
```
 reference.name(args);
 
```
    Parameters:
    
    reference - the ReferencePrefix the method is called on
    
    name - the MethodName
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on reference with arguments args
  - methodCall
```
public static MethodReference methodCall(ReferencePrefix reference,
                                         MethodName name,
                                         ImmutableArray<? extends Expression> args)
```
    Create a method call.
```
 reference.name(args);
 
```
    Parameters:
    
    reference - the ReferencePrefix the method is called on
    
    name - the MethodName
    
    args - the argument Expressions to be passed to the method
    
    Returns:
    
    a new MethodReference for call of method name on reference with arguments args
  - fieldReference
```
public static FieldReference fieldReference(Services services,
                                            java.lang.String name,
                                            Expression expression,
                                            ExecutionContext context)
```
    Create a field access.
```
 (expression).name
 
```
    Parameters:
    
    services - the Services to determine both expression 's KeYJavaType and the ProgramVariable corresponding to the field name
    
    name - the to be accessed field's name String
    
    expression - the Expression on which the field is accessed
    
    context - the ExecutionContext, which is needed to determine expression's KeYJavaType
    
    Returns:
    
    a new FieldReference of field name on expression
  - fieldReference
```
public static FieldReference fieldReference(ReferencePrefix prefix,
                                            ProgramVariable field)
```
    Create a field access.
```
 prefix.field
 
```
    Parameters:
    
    prefix - the ReferencePrefix on which field is accessed
    
    field - the ProgramVariable to be accessed
    
    Returns:
    
    a new FieldReference of field on prefix
  - finallyBlock
```
public static Finally finallyBlock(ExtList parameters)
```
    Create a finally block.
    
    Parameters:
    
    parameters - the finally block parameters (body) as ExtList
    
    Returns:
    
    a new Finally as defined by parameters
  - finallyBlock
```
public static Finally finallyBlock(Statement statement)
```
    Create a finally block.
```
 finally
     statement
 
```
    Parameters:
    
    statement - the Statement to be executed
    
    Returns:
    
    a new Finally block consisting of statement solely
  - finallyBlock
```
public static Finally finallyBlock(Statement[] statements)
```
    Create a finally block.
```
 finally {
     statements
 }
 
```
    Parameters:
    
    statements - the Statements to be executed
    
    Returns:
    
    a new Finally block consisting of statements solely
  - finallyBlock
```
public static Finally finallyBlock(StatementBlock body)
```
    Create a finally block.
```
 finally
     body
 
```
    Parameters:
    
    body - the StatementBlock to be executed
    
    Returns:
    
    a new Finally block consisting of body solely
  - declare
```
public static ProgramElement declare(ImmutableArray<Modifier> modifiers,
                                     IProgramVariable variable,
                                     Expression init,
                                     ProgramElementName typeName,
                                     int dimensions,
                                     ReferencePrefix typePrefix,
                                     KeYJavaType baseType)
```
    Create a local array variable declaration with an arbitrary number of modifiers.
```
 modifiers typePrefix.baseType[] variable = init;
 
```
    Parameters:
    
    modifiers - the Modifiers
    
    variable - the named and typed IProgramVariable to be declared
    
    init - the Expression variable is initialized with
    
    typeName - the type's ProgramElementName
    
    dimensions - the type's dimensions
    
    typePrefix - the type's ReferencePrefix
    
    baseType - the base KeYJavaType
    
    Returns:
    
    a new LocalVariableDeclaration of variable with static type baseType[dimensions] and initial value init
  - methodBody
```
public static MethodBodyStatement methodBody(JavaInfo model,
                                             ProgramVariable result,
                                             ReferencePrefix reference,
                                             KeYJavaType classType,
                                             java.lang.String methodName,
                                             ProgramVariable[] arguments)
```
    Create a method body shortcut. Note that classType is also used as visibility context when looking for methodName in its definition.
    
    Parameters:
    
    model - the JavaInfo that contains classType.methodName
    
    result - the ProgramVariable the return value is assigned to or null
    
    reference - the ReferencePrefix invocation target
    
    classType - the KeYJavaType in which the method is declared
    
    methodName - the method's String name
    
    arguments - the ProgramVariable and their static types the method is called with
    
    Returns:
    
    a new MethodBodyStatement for classType.methodName when called with arguments or null when the former is not defined
  - methodBody
```
public static MethodBodyStatement methodBody(ProgramVariable result,
                                             ReferencePrefix reference,
                                             IProgramMethod method,
                                             Expression[] arguments)
```
    Create a method body shortcut.
    
    Parameters:
    
    result - the ProgramVariable the return value is assigned to or null
    
    reference - the ReferencePrefix invocation target
    
    method - the IProgramMethod reference
    
    arguments - the Expressions and their static types the method is called with
    
    Returns:
    
    a new MethodBodyStatement for method when called with arguments
  - methodBody
```
public static MethodBodyStatement methodBody(ProgramVariable result,
                                             ReferencePrefix reference,
                                             IProgramMethod method,
                                             ImmutableArray<Expression> arguments)
```
    Create a method body shortcut.
    
    Parameters:
    
    result - the ProgramVariable the return value is assigned to or null
    
    reference - the ReferencePrefix invocation target
    
    method - the IProgramMethod reference
    
    arguments - the Expressions and their static types the method is called with
    
    Returns:
    
    a new MethodBodyStatement for method when called with arguments
  - methodFrame
```
public static MethodFrame methodFrame(IExecutionContext executionContext,
                                      StatementBlock block)
```
    Create a method call substitution.
    
    Parameters:
    
    executionContext - the block's IExecutionContext
    
    block - the StatementBlock to be put in executionContext
    
    Returns:
    
    a new MethodFrame that associates block with executionContext
  - methodFrame
```
public static MethodFrame methodFrame(IExecutionContext executionContext,
                                      StatementBlock block,
                                      PositionInfo position)
```
    Create a method call substitution at a specific source position.
    
    Parameters:
    
    executionContext - the block's IExecutionContext
    
    block - the StatementBlock to be put in executionContext
    
    position - the new source element's PositionInfo
    
    Returns:
    
    a new MethodFrame that associates block with executionContext and positions it at position
  - methodFrame
```
public static MethodFrame methodFrame(IProgramVariable result,
                                      IExecutionContext executionContext,
                                      StatementBlock block)
```
    Create a method call substitution with a return value assignment.
    
    Parameters:
    
    result - the IProgramVariable block's return value is assigned to
    
    executionContext - the block's IExecutionContext
    
    block - the StatementBlock to be put in executionContext
    
    Returns:
    
    a new MethodFrame that associates block with executionContext
  - methodFrame
```
public static MethodFrame methodFrame(IProgramVariable result,
                                      IExecutionContext executionContext,
                                      StatementBlock block,
                                      PositionInfo position)
```
    Create a method call substitution with a return value assignment at a specific source position.
    
    Parameters:
    
    result - the IProgramVariable block's return value is assigned to
    
    executionContext - the block's IExecutionContext
    
    block - the StatementBlock to be put in executionContext
    
    position - the new source element's PositionInfo
    
    Returns:
    
    a new MethodFrame that associates block with executionContext and positions it at position
  - intLiteral
```
public static IntLiteral intLiteral(java.lang.Integer value)
```
    Create an integer literal.
    
    Parameters:
    
    value - the Integer to be turned into an literal
    
    Returns:
    
    a new IntLiteral representing value
  - labeledStatement
```
public static LabeledStatement labeledStatement(ExtList parameters,
                                                Label label,
                                                PositionInfo position)
```
    Create a labeled statement.
    
    Parameters:
    
    parameters - the parameters (statement) as ExtList
    
    label - the Label
    
    position - the new source element's PositionInfo
    
    Returns:
    
    a new LabeledStatement as defined by parameters and label
  - labeledStatement
```
public static LabeledStatement labeledStatement(Label label,
                                                Statement statement,
                                                PositionInfo pos)
```
    Create a labeled statement.
```
 label: statement
 
```
    Parameters:
    
    label - the Label
    
    statement - the Statement to be labeled
    
    Returns:
    
    a new LabeledStatement that adds label to statement
  - labeledStatement
```
public static Statement labeledStatement(Label label,
                                         Statement[] statements,
                                         PositionInfo pos)
```
    Create a labeled block of statements.
```
 label: {
     statements
 }
 
```
    Parameters:
    
    label - the Label
    
    statements - the Statements to be labeled
    
    Returns:
    
    a new LabeledStatement that adds label to statements
  - newArray
```
public static NewArray newArray(TypeReference typeRef,
                                int dimensions,
                                Expression[] sizes,
                                ArrayInitializer initializer,
                                KeYJavaType keyJavaType)
```
    Create an array instantiation.
```
 new typeRef[sizes{1}]...[sizes{dimensions}] initializer
 
```
    Parameters:
    
    sizes - the size Expressions for each dimension
    
    typeRef - the static array base type
    
    keyJavaType - the array element type
    
    initializer - the ArrayInitializer
    
    dimensions - the number of dimensions
    
    Returns:
    
    a new NewArray for the instantiation of an array of base type typeRef with dimensions dimensions
  - newArray
```
public static NewArray newArray(TypeReference typeRef,
                                int dimensions,
                                Expression[] sizes,
                                KeYJavaType keyJavaType)
```
    Create an array instantiation.
```
 new typeRef[sizes{1}]...[sizes{dimensions}]
 
```
    Parameters:
    
    typeRef - the static array base type
    
    dimensions - the number of dimensions
    
    sizes - the size Expressions for each dimension
    
    keyJavaType - the array element type
    
    Returns:
    
    a new NewArray for the instantiation of an array of base type typeRef with dimensions dimensions
  - newArray
```
public static NewArray newArray(TypeReference typeRef,
                                int dimensions,
                                Expression size,
                                KeYJavaType keyJavaType)
```
    Create an array instantiation.
```
 new typeRef[size]
 
```
    Parameters:
    
    typeRef - the static array base type
    
    dimensions - the number of dimensions
    
    size - the size Expression for the first dimension
    
    keyJavaType - the array element type
    
    Returns:
    
    a new NewArray for the instantiation of an array of base type typeRef with dimensions dimensions
  - newArray
```
public static NewArray newArray(TypeReference typeRef,
                                int dimensions,
                                ArrayInitializer initializer,
                                KeYJavaType keyJavaType)
```
    Create an array instantiation.
```
 new typeRef[]...[] initializer
 
```
    Parameters:
    
    typeRef - the static array base type
    
    keyJavaType - the array element type
    
    initializer - the ArrayInitializer
    
    dimensions - the number of dimensions
    
    Returns:
    
    a new NewArray for the instantiation of an array of base type typeRef with dimensions dimensions
  - newOperator
```
public static New newOperator(ReferencePrefix referencePrefix,
                              TypeReference typeReference,
                              Expression[] args)
```
    Create an object allocation.
```
 new referencePrefix.typeReference(args)
 
```
    Parameters:
    
    referencePrefix - the typeReference's ReferencePrefix
    
    typeReference - a TypeReference to the class type that is instantiated
    
    args - the Expression arguments to be passed to the constructor
    
    Returns:
    
    a new New operator that allocates a new instance of typeReference parameterized with args
  - newOperator
```
public static New newOperator(ReferencePrefix referencePrefix,
                              KeYJavaType type,
                              Expression[] args)
```
    Create an object allocation.
```
 new referencePrefix.type(args)
 
```
    Parameters:
    
    referencePrefix - the type's ReferencePrefix
    
    type - the KeYJavaType to be instantiated
    
    args - the Expression arguments to be passed to the constructor
    
    Returns:
    
    a new New operator that allocates a new instance of type parameterized with args
  - newOperator
```
public static New newOperator(ReferencePrefix referencePrefix,
                              KeYJavaType type)
```
    Create an object allocation without arguments.
```
 new referencePrefix.type()
 
```
    Parameters:
    
    referencePrefix - the type's ReferencePrefix
    
    type - the KeYJavaType to be instantiated
    
    Returns:
    
    a new New operator that allocates a new instance of type
  - newOperator
```
public static New newOperator(KeYJavaType type)
```
    Create an object allocation without arguments.
```
 new type()
 
```
    Parameters:
    
    type - the KeYJavaType to be instantiated
    
    Returns:
    
    a new New operator that allocates a new instance of type
  - notEqualsOperator
```
public static NotEquals notEqualsOperator(ExtList operands)
```
    Create an unequal operator.
```
 operands{1} != operands{2}
 
```
    Parameters:
    
    operands - the operands ExtList
    
    Returns:
    
    a new NotEquals of operands
  - superConstructor
```
public static SuperConstructorReference superConstructor(ReferencePrefix referencePrefix,
                                                         Expression[] args)
```
    Create a call to the super constructor.
```
 super(args)
 
```
    Parameters:
    
    referencePrefix - the enclosing class type
    
    args - the Expression arguments to be passed to constructor
    
    Returns:
    
    a new SuperConstructorReference parameterized with args
  - superReference
```
public static SuperReference superReference()
```
    Create a reference to super.
    
    Returns:
    
    a new SuperReference
  - switchBlock
```
public static Switch switchBlock(Expression expression,
                                 Branch[] branches)
```
    Create a switch block.
```
 switch (expression) {
     branches
 }
 
```
    Parameters:
    
    expression - the to be evaluated Expression
    
    branches - the switch-case Branches
    
    Returns:
    
    a new Switch block that executes branches depending on the value of expression
  - switchBlock
```
public static Switch switchBlock(ExtList parameters)
```
    Create a switch block.
    
    Parameters:
    
    parameters - the switch-case parameters (guard, body, branches) as ExtList
    
    Returns:
    
    a new Switch as defined by parameters
  - synchronizedBlock
```
public static SynchronizedBlock synchronizedBlock(ExtList parameters)
```
    Create a synchronized block.
    
    Parameters:
    
    parameters - the synchronized block parameters (monitor, body) as ExtList
    
    Returns:
    
    a new SynchronizedBlock as defined by parameters
  - thenBlock
```
public static Then thenBlock(ExtList parameters)
```
    Create a then block.
    
    Parameters:
    
    parameters - the then block parameters (body) as ExtList
    
    Returns:
    
    a new Then as defined by parameters
  - thenBlock
```
public static Then thenBlock(Statement statement)
```
    Create a then block.
```
 then
     statement
 
```
    Parameters:
    
    statement - the to be executed Statement
    
    Returns:
    
    a new Then block that consists of statement solely
  - thenBlock
```
public static Then thenBlock(Statement[] statements)
```
    Create a then block.
```
 then {
     statements
 }
 
```
    Parameters:
    
    statements - the to be executed Statements
    
    Returns:
    
    a new Then block that consists of statements solely
  - thisConstructor
```
public static ThisConstructorReference thisConstructor(Expression[] args)
```
    Create a call to a constructor of the current class.
```
 this(args)
 
```
    Parameters:
    
    args - the Expression arguments to be passed to constructor
    
    Returns:
    
    a new ThisConstructorReference parameterized with args
  - thisReference
```
public static ThisReference thisReference()
```
    Create a reference to this.
    
    Returns:
    
    a new ThisReference
  - trueLiteral
```
public static BooleanLiteral trueLiteral()
```
    Create a literal for the truth value true.
    
    Returns:
    
    a BooleanLiteral that represents the value true
  - tryBlock
```
public static Try tryBlock(ExtList parameters)
```
    Create a try block.
    
    Parameters:
    
    parameters - the try-catch parameters (body, branches) as ExtList
    
    Returns:
    
    a new Try as defined by parameters
  - tryBlock
```
public static Try tryBlock(StatementBlock body,
                           Branch[] branches)
```
    Create a try block.
```
 try
     body
 branches
 
```
    Parameters:
    
    body - the StatementBlock to be executed
    
    branches - the try-catch Branches
    
    Returns:
    
    a new Try block for the execution of branches depending on the events during the execution of body
  - tryBlock
```
public static Try tryBlock(Statement statement,
                           Branch[] branches)
```
    Create a try block.
```
 try
     statement
 branches
 
```
    Parameters:
    
    statement - the Statement to be executed
    
    branches - the try-catch Branches
    
    Returns:
    
    a new Try block for the execution of branches depending on the events during the execution of statement
  - tryBlock
```
public static Try tryBlock(Statement statement,
                           Branch branch)
```
    Create a try block.
```
 try
     statement
 branch
 
```
    Parameters:
    
    statement - the Statement to be executed
    
    branches - the try-catch Branch
    
    Returns:
    
    a new Try block for the execution of branch depending on the events during the execution of statement
  - typeRef
```
public static TypeRef typeRef(KeYJavaType type)
```
    Create a type reference.
```
 type
 
```
    Parameters:
    
    type - the KeYJavaType to be referenced
    
    Returns:
    
    a new TypeRef that references type
  - typeRef
```
public static TypeRef typeRef(KeYJavaType type,
                              int dimensions)
```
    Create a type reference.
```
 type[]...[]
 
```
    Parameters:
    
    type - the base KeYJavaType
    
    dimensions - the number of dimensions
    
    Returns:
    
    a new TypeRef for dimensions dimensions of type
  - falseLiteral
```
public static BooleanLiteral falseLiteral()
```
    Create a literal for the truth value false.
    
    Returns:
    
    a BooleanLiteral that represents the value true
  - variableSpecification
```
public static VariableSpecification variableSpecification(IProgramVariable variable,
                                                          int dimensions,
                                                          Expression initializer,
                                                          Type type)
```
    Create a variable specification.
    
    Parameters:
    
    variable - the IProgramVariable to be specified
    
    dimensions - the number of dimensions
    
    initializer - the initializer Expression
    
    type - the Type
    
    Returns:
    
    a new VariableSpecification for variable of type type[dimensions], initialized to initializer
  - variableSpecification
```
public static VariableSpecification variableSpecification(IProgramVariable variable,
                                                          Expression initializer,
                                                          KeYJavaType keyJavaType)
```
    Create a variable specification.
    
    Parameters:
    
    variable - the IProgramVariable to be specified
    
    initializer - the initializer Expression
    
    keyJavaType - the KeYJavaType
    
    Returns:
    
    a new VariableSpecification for variable of type type, initialized to initializer
  - zeroLiteral
```
public static IntLiteral zeroLiteral()
```
    Create a literal for the integer zero.
```
 0
 
```
    Returns:
    
    a new IntLiteral that represents the integer value 0
  - cast
```
public static TypeCast cast(Expression expression,
                            KeYJavaType targetType)
```

Class KeYJavaASTFactory

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Detail

KeYJavaASTFactory

Method Detail

assign

assign

assign

attribute

declare

declare

declare

declare

declare

declare

declare

parameterDeclaration

parameterDeclaration

parameterDeclaration

parenthesizedExpression

passiveExpression

localVariable

localVariable

localVariable

logicalAndOperator

logicalOrOperator

catchClause

catchClause

catchClause

catchClause

catchClause

throwClause

transactionStatement

trueGuard

whileLoop

whileLoop

returnClause

ifThen

ifThen

ifThen

ifStatement

ifElse

ifElse

breakStatement

breakStatement

caseBlock

caseBlock

caseBlock

continueStatement

emptyStatement

enhancedForLoop

equalsNullOperator

equalsOperator

equalsOperator

executionContext

insertStatementInBlock

insertStatementInBlock

insertStatementInBlock

insertStatementInBlock

instanceOf

declareZero

declareMethodCall

declareMethodCall

defaultBlock

defaultBlock

defaultBlock

doLoop

elseBlock

elseBlock

elseBlock

loopInit

loopInitZero

arrayInitializer

arrayLength

lessThanGuard

lessThanOperator

lessThanZeroOperator

lessThanArrayLengthGuard