| 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.ProgramMetaConstruct
All known Subclasses: de.uka.ilkd.key.rule.metaconstruct.InitArray, de.uka.ilkd.key.rule.metaconstruct.MethodCall, de.uka.ilkd.key.rule.metaconstruct.ExpandMethodBody, de.uka.ilkd.key.rule.metaconstruct.UnwindLoop, de.uka.ilkd.key.rule.metaconstruct.ConstructorCall, de.uka.ilkd.key.rule.metaconstruct.SpecialConstructorCall, de.uka.ilkd.key.rule.metaconstruct.StaticInitialisation, de.uka.ilkd.key.rule.metaconstruct.EvaluateArgs, de.uka.ilkd.key.rule.metaconstruct.Unpack, de.uka.ilkd.key.rule.metaconstruct.IsStatic, de.uka.ilkd.key.rule.metaconstruct.ArrayLength, de.uka.ilkd.key.rule.metaconstruct.CreateObject, de.uka.ilkd.key.rule.metaconstruct.TypeOf, de.uka.ilkd.key.rule.metaconstruct.PostWork, de.uka.ilkd.key.rule.metaconstruct.SwitchToIf, de.uka.ilkd.key.rule.metaconstruct.ArrayPostDecl, de.uka.ilkd.key.rule.metaconstruct.DoBreak, de.uka.ilkd.key.rule.metaconstruct.MultipleVarDecl,
| ProgramMetaConstruct | | abstract public class ProgramMetaConstruct extends JavaNonTerminalProgramElement implements StatementContainer,Statement,Expression,TypeReference(Code) | | Program meta constructs are used for schematic transformations that
cannot be expressed in form of schematic formulas of taclets. For
example:
- transformations needing access to the java (type) model, e.g
dynamic dispatch of program methods
- 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.
|
| ProgramMetaConstruct | | public ProgramMetaConstruct(Name name, ProgramElement body)(Code) | | creates a ProgramMetaConstruct
Parameters:
name - the Name of the meta construct
Parameters:
body - the ProgramElement contained by the meta construct |
| ProgramMetaConstruct | | public ProgramMetaConstruct(String name, ProgramElement body)(Code) | | creates a ProgramMetaConstruct
Parameters:
name - the String with the name of the meta construct
Parameters:
body - the ProgramElement contained by the meta construct |
| body | | public ProgramElement body()(Code) | | returns the body of the meta construct
the body of the meta construct |
| getChildAt | | public ProgramElement getChildAt(int index)(Code) | | Returns the child at the specified index in this node's "virtual"
child array.
Parameters:
index - an index into this node's "virtual" child array the program element at the given position
exception:
ArrayIndexOutOfBoundsException - if index is outof bounds |
| getChildCount | | public int getChildCount()(Code) | | Returns the number of children of this node.
an int giving the number of children of this node |
| getDimensions | | public int getDimensions()(Code) | | |
| getExpressionCount | | public int getExpressionCount()(Code) | | |
| getLastElement | | public SourceElement getLastElement()(Code) | | Finds the source element that occurs last in the source.
the last source element in the syntactical representation ofthis element, may be equals to this element. |
| getStatementCount | | public int getStatementCount()(Code) | | Get the number of statements in this container.
the number of statements. |
| getTypeReferenceCount | | public int getTypeReferenceCount()(Code) | | |
| name | | public Name name()(Code) | | returns the name of the meta construct
the name of the meta construct |
| symbolicExecution | | abstract public ProgramElement symbolicExecution(ProgramElement pe, Services services, SVInstantiations svInst)(Code) | | performs the program transformation needed for symbolic
program transformation
Parameters:
pe - the ProgramElement on which the execution is performed
Parameters:
services - the Services with all necessary information about the java programs
Parameters:
svInst - the instantiations of the schemavariables the transformated program |
| visit | | public void visit(Visitor v)(Code) | | calls the corresponding method of a visitor in order to
perform some action/transformation on this element
Parameters:
v - the Visitor |
|
|