All Methods Static Methods Instance Methods Concrete Methods
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 Map<Term,PosInOccurrence> |
collectBaseOccs(Term focus,
Sequent seq) |
private static void |
collectBaseOccsHelper(Term focus,
PosInOccurrence pos,
Map<Term,PosInOccurrence> result) |
UseDependencyContractApp |
createApp(PosInOccurrence pos) |
UseDependencyContractApp |
createApp(PosInOccurrence pos,
TermServices services) |
String |
displayName()
returns the display name of the rule
|
static PosInOccurrence |
findStepInIfInsts(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 List<Term> |
getEqualityDefs(Term term,
Sequent seq) |
private static 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,
List<Term> result) |
static List<PosInOccurrence> |
getSteps(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
|
String |
toString() |