public class CreateObject extends ProgramTransformer
new Class(...)
occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created>
to
true
as well as setting all fields of the object to their
default values. For the complete procedure, the method creates the
implicit method <createObject>
which on its part calls
another implicit method lt;prepare>
for setting the fields
values.Constructor and Description |
---|
CreateObject(ProgramElement newExpr) |
Modifier and Type | Method and Description |
---|---|
ProgramElement |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
creates and returns a method reference to the implicit '
|
body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, neededInstantiations, needs, prettyPrint, setReferencePrefix, toString, visit
compatibleBlockSize, equals, equalsModRenaming, getArrayPos, hashCode, match, matchChildren
getComments, prettyPrintMain, reuseSignature
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
public CreateObject(ProgramElement newExpr)
public ProgramElement transform(ProgramElement pe, Services services, SVInstantiations svInst)
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programssvInst
- the instantiations of the schemavariables