de.uka.ilkd.key.rule.metaconstruct

Class ForToWhile

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.ForToWhile

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 ForToWhile
extends ProgramTransformer

converts a for-loop to a while loop. Invariant and other rules cannot be performed on for but only on while loops. It makes uses of the ForToWhileTransformation to create a transformed loop body which is then put into the corresponding context.

Example

 for (int i = 0; i < 100; i++) {
     if (i == 2)
         continue;
     if (i == 3)
         break;
 }
 

is translated to

 _label1: {
     int i = 0;
     while (i < 100) {
         _label0: {
             if (i == 2)
                 break _label0;
             if (i == 3)
                 break _label1;
         }
         i++;
     }
 }
 

Author:

MU

See Also:

ForToWhileTransformation

Field Summary

Fields

Modifier and Type	Field and Description
private SchemaVariable	innerLabel the inner label ('l2')
private SchemaVariable	outerLabel the outer label that is used to leave the while loop ('l1')

Constructor Summary

Constructors

Constructor and Description
ForToWhile(SchemaVariable innerLabel, SchemaVariable outerLabel, Statement loop) creates an loop to while - ProgramTransformer

Method Summary

Modifier and Type	Method and Description
ImmutableList<SchemaVariable>	neededInstantiations(SVInstantiations svInst) return a list of the SV that are relevant to this UnwindLoop
ProgramElement[]	transform(ProgramElement pe, Services services, SVInstantiations svInst) 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, 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

Field Detail

outerLabel

private final SchemaVariable outerLabel

the outer label that is used to leave the while loop ('l1')

innerLabel

private final SchemaVariable innerLabel

the inner label ('l2')

Constructor Detail

ForToWhile

public ForToWhile(SchemaVariable innerLabel,
                  SchemaVariable outerLabel,
                  Statement loop)

creates an loop to while - ProgramTransformer

Parameters:

loop - the LoopStatement contained by the meta construct

innerLabel - the label used to handle continue

outerLabel - the label used to handle break (only needed for do-while-loops)

Method Detail

transform

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

Description copied from class: ProgramTransformer

performs the program transformation needed for symbolic program transformation

Specified by:

transform in class ProgramTransformer

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

neededInstantiations

public ImmutableList<SchemaVariable> neededInstantiations(SVInstantiations svInst)

return a list of the SV that are relevant to this UnwindLoop

Overrides:

neededInstantiations in class ProgramTransformer

Parameters:

svInst - the instantiations so far - ignored

Returns:

a list of 0 to 2 schema variables (outer/inner label)