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
.
Modifier and Type | Field and Description |
---|---|
static LoopApplyHeadRule |
INSTANCE
The only instance of this class.
|
static Name |
NAME
The rule name.
|
Constructor and Description |
---|
LoopApplyHeadRule() |
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() |
public static final LoopApplyHeadRule INSTANCE
public static final Name NAME
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp application) throws RuleAbortException
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsapplication
- the rule application to be executedRuleAbortException
public java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule