de.uka.ilkd.key.rule

Class LoopApplyHeadRule

java.lang.Object

de.uka.ilkd.key.rule.LoopApplyHeadRule

All Implemented Interfaces:

BuiltInRule, Rule

public class LoopApplyHeadRule
extends java.lang.Object
implements BuiltInRule

This rule transforms a block that starts with a for loop into one that starts with a while loop.

This is necessary because the rules for loop contracts (subclasses of AbstractLoopContractRule) can only be applied on blocks that start with a while loop.

The transformation is equivalent to the ForToWhileTransformation, the only difference being that we transform the whole block containing the loop instead of just the loop itself. This is implemented as a built-in rule because the opening brace of the block on which it is applied belongs to the non-active prefix and thus cannot be matched by the taclet language.

Note that the actual transformation is performed in the constructor of LoopContractImpl.

Author:

lanzinger

Field Summary

Fields

Modifier and Type	Field and Description
static LoopApplyHeadRule	INSTANCE The only instance of this class.
static Name	NAME The rule name.

Constructor Summary

Constructors

Constructor and Description
LoopApplyHeadRule()

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp application) the rule is applied on the given goal using the information of rule application.
IBuiltInRuleApp	createApp(PosInOccurrence pos, TermServices services)
java.lang.String	displayName() returns the display name of the rule
boolean	isApplicable(Goal goal, PosInOccurrence pio) returns true iff a rule is applicable at the given position.
boolean	isApplicableOnSubTerms()
Name	name() the name of the rule
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

INSTANCE

public static final LoopApplyHeadRule INSTANCE

The only instance of this class.

NAME

public static final Name NAME

The rule name.

Constructor Detail

LoopApplyHeadRule

public LoopApplyHeadRule()

Method Detail

apply

public ImmutableList<Goal> apply(Goal goal,
                                 Services services,
                                 RuleApp application)
                          throws RuleAbortException

Description copied from interface: Rule

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface Rule

Parameters:

goal - the Goal on which to apply ruleApp

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

application - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

Throws:

RuleAbortException

name

public Name name()

Description copied from interface: Rule

the name of the rule

Specified by:

name in interface Rule

displayName

public java.lang.String displayName()

Description copied from interface: Rule

returns the display name of the rule

Specified by:

displayName in interface Rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

createApp

public IBuiltInRuleApp createApp(PosInOccurrence pos,
                                 TermServices services)

Specified by:

createApp in interface BuiltInRule

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence pio)

Description copied from interface: BuiltInRule

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

Specified by:

isApplicable in interface BuiltInRule

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule