de.uka.ilkd.key.rule

Class UseDependencyContractRule

java.lang.Object

de.uka.ilkd.key.rule.UseDependencyContractRule

All Implemented Interfaces:

BuiltInRule, Rule

public final class UseDependencyContractRule
extends java.lang.Object
implements BuiltInRule

Field Summary

Fields

Modifier and Type	Field and Description
static UseDependencyContractRule	INSTANCE
private static Name	NAME

Constructor Summary

Constructors

Modifier	Constructor and Description
private	UseDependencyContractRule()

Method Summary

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()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

INSTANCE

public static final UseDependencyContractRule INSTANCE

NAME

private static final Name NAME

Constructor Detail

UseDependencyContractRule

private UseDependencyContractRule()

Method Detail

getEqualityDefs

private static java.util.List<Term> getEqualityDefs(Term term,
                                                    Sequent seq)

getEqualityDefsAndPos

private static java.util.List<Pair<Term,PosInOccurrence>> getEqualityDefsAndPos(Term term,
                                                                                Sequent seq)

addEqualDefs

private ImmutableSet<Term> addEqualDefs(ImmutableSet<Term> terms,
                                        Goal g)

hasRawSteps

private boolean hasRawSteps(Term heapTerm,
                            Sequent seq,
                            Services services)

getRawSteps

private static void getRawSteps(Term heapTerm,
                                Sequent seq,
                                Services services,
                                java.util.List<Term> result)

getFreshLocsStep

private static PosInOccurrence getFreshLocsStep(PosInOccurrence heapPos,
                                                Sequent seq,
                                                Services services)

getChangedLocsForStep

private static Pair<Term,ImmutableList<PosInOccurrence>> getChangedLocsForStep(Term heapTerm,
                                                                               Term stepHeap,
                                                                               Sequent seq,
                                                                               Services services)

isBaseOcc

public static boolean isBaseOcc(Term focus,
                                Term candidate)

collectBaseOccsHelper

private static void collectBaseOccsHelper(Term focus,
                                          PosInOccurrence pos,
                                          java.util.Map<Term,PosInOccurrence> result)

collectBaseOccs

private static java.util.Map<Term,PosInOccurrence> collectBaseOccs(Term focus,
                                                                   Sequent seq)

getSteps

public static java.util.List<PosInOccurrence> getSteps(java.util.List<LocationVariable> heapContext,
                                                       PosInOccurrence pos,
                                                       Sequent seq,
                                                       Services services)

findStepInIfInsts

public static PosInOccurrence findStepInIfInsts(java.util.List<PosInOccurrence> steps,
                                                UseDependencyContractApp app,
                                                TermServices services)

getApplicableContracts

public static ImmutableSet<Contract> getApplicableContracts(Services services,
                                                            KeYJavaType kjt,
                                                            IObserverFunction target)

Returns the dependency contracts which are applicable for the passed target.

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence pio)

Description copied from interface: BuiltInRule

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

Specified by:

isApplicable in interface BuiltInRule

apply

public ImmutableList<Goal> apply(Goal goal,
                                 Services services,
                                 RuleApp ruleApp)

Description copied from interface: Rule

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface Rule

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

name

public Name name()

Description copied from interface: Rule

the name of the rule

Specified by:

name in interface Rule

displayName

public java.lang.String displayName()

Description copied from interface: Rule

returns the display name of the rule

Specified by:

displayName in interface Rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

createApp

public UseDependencyContractApp createApp(PosInOccurrence pos)

createApp

public UseDependencyContractApp createApp(PosInOccurrence pos,
                                          TermServices services)

Specified by:

createApp in interface BuiltInRule

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule