de.uka.ilkd.key.rule.metaconstruct

Class ProgramTransformer

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, Reference, MemberReference, NameReference, PackageReferenceContainer, ReferencePrefix, ReferenceSuffix, TypeReference, TypeReferenceContainer, TypeReferenceInfix, SourceElement, Statement, StatementContainer, SVSubstitute

Direct Known Subclasses:

ArrayLength, ArrayPostDecl, ConstructorCall, CreateObject, DoBreak, EnhancedForElimination, EvaluateArgs, ExpandMethodBody, ForInitUnfoldTransformer, ForToWhile, InitArray, IsStatic, MethodCall, MultipleVarDecl, PostWork, SpecialConstructorCall, StaticInitialisation, SwitchToIf, TypeOf, Unpack, UnwindLoop

public abstract class ProgramTransformer
extends JavaNonTerminalProgramElement
implements StatementContainer, Statement, Expression, TypeReference

ProgramTransformers are used to describe schematic transformations that cannot be expressed by the taclet language itself. For example:

1. transformations needing access to the java (type) model, e.g dynamic dispatch of program methods
2. complex transformations that are hard (or not) to express via taclets, for example unwinding a loop (together with replacing continues or unlabeled breaks with a labeled break)

(Program)MetaConstructs should be used with care as they make it hard to validate (verify) rules and import nearly the complete power of Java into taclets.

Field Summary

Fields

Modifier and Type	Field and Description
private ProgramElement	body the encapsulated program element
private Name	name the name of the meta construct

Constructor Summary

Constructors

Constructor and Description
ProgramTransformer(Name name, ProgramElement body) creates a ProgramTransformer
ProgramTransformer(java.lang.String name, ProgramElement body) creates a ProgramTransformer

Method Summary

Modifier and Type	Method and Description
ProgramElement	body() returns the body of the meta construct
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array.
int	getChildCount() Returns the number of children of this node.
int	getDimensions()
Expression	getExpressionAt(int index)
int	getExpressionCount() Get the number of expressions in this container.
KeYJavaType	getKeYJavaType()
KeYJavaType	getKeYJavaType(Services javaServ, ExecutionContext ec) returns the KeYJavaType of an expression
KeYJavaType	getKeYJavaType(TermServices javaServ)
SourceElement	getLastElement() Finds the source element that occurs last in the source.
java.lang.String	getName() Return the name of the model element.
PackageReference	getPackageReference() Get the package reference.
ProgramElementName	getProgramElementName() Get identifier.
ReferencePrefix	getReferencePrefix()
Statement	getStatementAt(int index)
int	getStatementCount() Get the number of statements in this container.
TypeReference	getTypeReferenceAt(int index)
int	getTypeReferenceCount() Get the number of type references in this container.
Name	name() returns the name of the meta construct
ImmutableList<SchemaVariable>	neededInstantiations(SVInstantiations svInst) get a list of schema variables that are needed by this entity when working given a SV instantiation set.
ImmutableList<SchemaVariable>	needs() get a list of schema variables that are needed by this entity when working given a SV instantiation set.
void	prettyPrint(PrettyPrinter p) Pretty printing the source element.
ReferencePrefix	setReferencePrefix(ReferencePrefix r)
java.lang.String	toString() to String
abstract ProgramElement[]	transform(ProgramElement pe, Services services, SVInstantiations svInst) performs the program transformation needed for symbolic program transformation
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Field Detail

name

private Name name

the name of the meta construct

body

private ProgramElement body

the encapsulated program element

Constructor Detail

ProgramTransformer

public ProgramTransformer(Name name,
                          ProgramElement body)

creates a ProgramTransformer

Parameters:

name - the Name of the meta construct

body - the ProgramElement contained by the meta construct

ProgramTransformer

public ProgramTransformer(java.lang.String name,
                          ProgramElement body)

creates a ProgramTransformer

Parameters:

name - the String with the name of the meta construct

body - the ProgramElement contained by the meta construct

Method Detail

transform

public abstract ProgramElement[] transform(ProgramElement pe,
                                           Services services,
                                           SVInstantiations svInst)

performs the program transformation needed for symbolic program transformation

Parameters:

pe - the ProgramElement on which the execution is performed

services - the Services with all necessary information about the java programs

svInst - the instantiations of the schemavariables

Returns:

the transformated program

name

public Name name()

returns the name of the meta construct

Returns:

the name of the meta construct

body

public ProgramElement body()

returns the body of the meta construct

Returns:

the body of the meta construct

getLastElement

public SourceElement getLastElement()

Finds the source element that occurs last in the source.

Specified by:

getLastElement in interface SourceElement

Overrides:

getLastElement in class JavaSourceElement

Returns:

the last source element in the syntactical representation of this element, may be equals to this element.

See Also:

JavaSourceElement.toSource(), JavaSourceElement.getEndPosition()

getStatementCount

public int getStatementCount()

Get the number of statements in this container.

Specified by:

getStatementCount in interface StatementContainer

Returns:

the number of statements.

getStatementAt

public Statement getStatementAt(int index)

Specified by:

getStatementAt in interface StatementContainer

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Returns:

an int giving the number of children of this node

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array.

Specified by:

getChildAt in interface NonTerminalProgramElement

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

getReferencePrefix

public ReferencePrefix getReferencePrefix()

Specified by:

getReferencePrefix in interface ReferencePrefix

Specified by:

getReferencePrefix in interface TypeReference

setReferencePrefix

public ReferencePrefix setReferencePrefix(ReferencePrefix r)

getDimensions

public int getDimensions()

Specified by:

getDimensions in interface TypeReference

getTypeReferenceCount

public int getTypeReferenceCount()

Description copied from interface: TypeReferenceContainer

Get the number of type references in this container.

Specified by:

getTypeReferenceCount in interface TypeReferenceContainer

Returns:

the number of type references.

getTypeReferenceAt

public TypeReference getTypeReferenceAt(int index)

Specified by:

getTypeReferenceAt in interface TypeReferenceContainer

getPackageReference

public PackageReference getPackageReference()

Description copied from interface: PackageReferenceContainer

Get the package reference.

Specified by:

getPackageReference in interface PackageReferenceContainer

Returns:

the package reference.

getExpressionCount

public int getExpressionCount()

Description copied from interface: ExpressionContainer

Get the number of expressions in this container.

Specified by:

getExpressionCount in interface ExpressionContainer

Returns:

the number of expressions.

getExpressionAt

public Expression getExpressionAt(int index)

Specified by:

getExpressionAt in interface ExpressionContainer

getProgramElementName

public ProgramElementName getProgramElementName()

Description copied from interface: NamedProgramElement

Get identifier.

Specified by:

getProgramElementName in interface NamedProgramElement

Specified by:

getProgramElementName in interface TypeReference

Returns:

the identifier.

getName

public java.lang.String getName()

Description copied from interface: NamedModelElement

Return the name of the model element.

Specified by:

getName in interface NamedModelElement

Specified by:

getName in interface TypeReference

Returns:

the name of the model element.

visit

public void visit(Visitor v)

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

toString

public java.lang.String toString()

to String

Overrides:

toString in class JavaSourceElement

getKeYJavaType

public KeYJavaType getKeYJavaType()

Specified by:

getKeYJavaType in interface TypeReference

getKeYJavaType

public KeYJavaType getKeYJavaType(TermServices javaServ)

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ,
                                  ExecutionContext ec)

Description copied from interface: Expression

returns the KeYJavaType of an expression

Specified by:

getKeYJavaType in interface Expression

needs

public ImmutableList<SchemaVariable> needs()

get a list of schema variables that are needed by this entity when working given a SV instantiation set.

Parameters:

svInst - the instantiations of SV so far.

Returns:

a list of schema variables relevant for this entity;

neededInstantiations

public ImmutableList<SchemaVariable> neededInstantiations(SVInstantiations svInst)

get a list of schema variables that are needed by this entity when working given a SV instantiation set.

Parameters:

svInst - the instatiations of SV so far.

Returns:

a list of schema variables relevant for this entity;