public final class UseDependencyContractRule extends java.lang.Object implements BuiltInRule
Modifier and Type | Field and Description |
---|---|
static UseDependencyContractRule |
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.
|
UseDependencyContractApp |
createApp(PosInOccurrence pos) |
UseDependencyContractApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
static PosInOccurrence |
findStepInIfInsts(java.util.List<PosInOccurrence> steps,
UseDependencyContractApp app,
TermServices services) |
static ImmutableSet<Contract> |
getApplicableContracts(Services services,
KeYJavaType kjt,
IObserverFunction target)
Returns the dependency contracts which are applicable for the passed
target.
|
static java.util.List<PosInOccurrence> |
getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
static boolean |
isBaseOcc(Term focus,
Term candidate) |
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 UseDependencyContractRule INSTANCE
public static java.util.List<PosInOccurrence> getSteps(java.util.List<LocationVariable> heapContext, PosInOccurrence pos, Sequent seq, Services services)
public static PosInOccurrence findStepInIfInsts(java.util.List<PosInOccurrence> steps, UseDependencyContractApp app, TermServices services)
public static ImmutableSet<Contract> getApplicableContracts(Services services, KeYJavaType kjt, IObserverFunction target)
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
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 executedpublic java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public UseDependencyContractApp createApp(PosInOccurrence pos)
public UseDependencyContractApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
Copyright © 2003-2019 The KeY-Project.