de.uka.ilkd.key.rule.metaconstruct

Class DoBreak

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

de.uka.ilkd.key.rule.metaconstruct.DoBreak

All Implemented Interfaces:

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

public class DoBreak
extends ProgramTransformer

This class performs a labeled break. This means l1:l2:{l3:{l4:{break l3;}} ...} becomes l1:l2:{...}

Constructor Summary

Constructors

Constructor and Description
DoBreak(LabeledStatement labeledBreak) creates a do-break ProgramTransformer

Method Summary

Modifier and Type	Method and Description
private ProgramElement	doBreak(NonTerminalProgramElement block, Label breakLabel, Break b) a helper method to perform the symbolic execution of the doBreak metaconstruct.
ProgramElement[]	transform(ProgramElement pe, Services services, SVInstantiations insts) performs the program transformation needed for symbolic program transformation

Methods inherited from class de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

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

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

Constructor Detail

DoBreak

public DoBreak(LabeledStatement labeledBreak)

creates a do-break ProgramTransformer

Parameters:

labeledBreak - the LabeledStatement contained by the meta construct

Method Detail

doBreak

private ProgramElement doBreak(NonTerminalProgramElement block,
                               Label breakLabel,
                               Break b)

a helper method to perform the symbolic execution of the doBreak metaconstruct.

Parameters:

block - the NonTerminalProgramElement to go through and look for the label

breakLabel - the Label the break statement marked

transform

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

performs the program transformation needed for symbolic program transformation

Specified by:

transform in class ProgramTransformer

Parameters:

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

pe - the ProgramElement on which the execution is performed

insts - the instantiations of the schemavariables

Returns:

the transformated program