public final class WhileInvariantRule extends java.lang.Object implements BuiltInRule
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
BODY_PRESERVES_INVARIANT_LABEL |
static java.lang.String |
FULL_INVARIANT_TERM_HINT
The unit used to refactor the full invariant.
|
static java.lang.String |
INITIAL_INVARIANT_ONLY_HINT
The hint used to refactor the initial invariant.
|
static WhileInvariantRule |
INSTANCE |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
LoopInvariantBuiltInRuleApp |
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() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final java.lang.String INITIAL_INVARIANT_ONLY_HINT
public static final java.lang.String FULL_INVARIANT_TERM_HINT
public static final WhileInvariantRule INSTANCE
public static final java.lang.String BODY_PRESERVES_INVARIANT_LABEL
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- 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 LoopInvariantBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
Copyright © 2003-2019 The KeY-Project.