public final class UseDependencyContractRule extends java.lang.Object implements BuiltInRule
Modifier and Type | Field and Description |
---|---|
static UseDependencyContractRule |
INSTANCE |
private static Name |
NAME |
Modifier | Constructor and Description |
---|---|
private |
UseDependencyContractRule() |
Modifier and Type | Method and Description |
---|---|
private ImmutableSet<Term> |
addEqualDefs(ImmutableSet<Term> terms,
Goal g) |
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
private static java.util.Map<Term,PosInOccurrence> |
collectBaseOccs(Term focus,
Sequent seq) |
private static void |
collectBaseOccsHelper(Term focus,
PosInOccurrence pos,
java.util.Map<Term,PosInOccurrence> result) |
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.
|
private static Pair<Term,ImmutableList<PosInOccurrence>> |
getChangedLocsForStep(Term heapTerm,
Term stepHeap,
Sequent seq,
Services services) |
private static java.util.List<Term> |
getEqualityDefs(Term term,
Sequent seq) |
private static java.util.List<Pair<Term,PosInOccurrence>> |
getEqualityDefsAndPos(Term term,
Sequent seq) |
private static PosInOccurrence |
getFreshLocsStep(PosInOccurrence heapPos,
Sequent seq,
Services services) |
private static void |
getRawSteps(Term heapTerm,
Sequent seq,
Services services,
java.util.List<Term> result) |
static java.util.List<PosInOccurrence> |
getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
private boolean |
hasRawSteps(Term heapTerm,
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() |
public static final UseDependencyContractRule INSTANCE
private static final Name NAME
private static java.util.List<Pair<Term,PosInOccurrence>> getEqualityDefsAndPos(Term term, Sequent seq)
private ImmutableSet<Term> addEqualDefs(ImmutableSet<Term> terms, Goal g)
private static void getRawSteps(Term heapTerm, Sequent seq, Services services, java.util.List<Term> result)
private static PosInOccurrence getFreshLocsStep(PosInOccurrence heapPos, Sequent seq, Services services)
private static Pair<Term,ImmutableList<PosInOccurrence>> getChangedLocsForStep(Term heapTerm, Term stepHeap, Sequent seq, Services services)
private static void collectBaseOccsHelper(Term focus, PosInOccurrence pos, java.util.Map<Term,PosInOccurrence> result)
private static java.util.Map<Term,PosInOccurrence> collectBaseOccs(Term focus, Sequent seq)
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