public final class UseOperationContractRule extends java.lang.Object implements BuiltInRule
Modifier and Type | Class and Description |
---|---|
static class |
UseOperationContractRule.Instantiation |
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
FINAL_PRE_TERM_HINT
Hint to refactor the final pre term.
|
static UseOperationContractRule |
INSTANCE
A static instance of the (built-in) operation contract rule application.
|
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.
|
static java.util.Map<LocationVariable,LocationVariable> |
computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
static UseOperationContractRule.Instantiation |
computeInstantiation(Term focusTerm,
Services services)
Computes instantiation for contract rule on passed focus term.
|
static ImmutableList<Term> |
computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static ProgramVariable |
computeResultVar(UseOperationContractRule.Instantiation inst,
TermServices services)
Computes the result variable for this instantiation.
|
static Term |
computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf)
Returns the correct self term.
|
ContractRuleApp |
createApp(PosInOccurrence pos) |
ContractRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
static ImmutableSet<FunctionalOperationContract> |
getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services)
Returns the operation contracts which are applicable for the passed instantiation.
|
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 FINAL_PRE_TERM_HINT
public static final UseOperationContractRule INSTANCE
public static ImmutableSet<FunctionalOperationContract> getApplicableContracts(UseOperationContractRule.Instantiation inst, Services services)
inst
- the operation contract rule instantiationservices
- the services objectpublic static UseOperationContractRule.Instantiation computeInstantiation(Term focusTerm, Services services)
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 ContractRuleApp createApp(PosInOccurrence pos)
public ContractRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public static java.util.Map<LocationVariable,LocationVariable> computeAtPreVars(java.util.List<LocationVariable> heapContext, TermServices services, UseOperationContractRule.Instantiation inst)
heapContext
- the heap variablesservices
- the services objectinst
- the instantiation for the operation contract rulepublic static Term computeSelf(Term baseHeapTerm, java.util.Map<LocationVariable,Term> atPres, LocationVariable baseHeap, UseOperationContractRule.Instantiation inst, Term resultTerm, TermFactory tf)
baseHeapTerm
- the heap termatPres
- the pre-heap variables as termsbaseHeap
- the heap variableinst
- the instantiation for the operation contract ruleresultTerm
- the term of the result variabletf
- the term factorypublic static ImmutableList<Term> computeParams(Term baseHeapTerm, java.util.Map<LocationVariable,Term> atPres, LocationVariable baseHeap, UseOperationContractRule.Instantiation inst, TermFactory tf)
baseHeapTerm
- the heap termatPres
- the pre-heap variables as termsbaseHeap
- the heap variableinst
- the instantiation for the operation contract ruletf
- the term factorypublic static ProgramVariable computeResultVar(UseOperationContractRule.Instantiation inst, TermServices services)
inst
- the instantiation for the operation contract ruleservices
- the services objectpublic boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
Copyright © 2003-2019 The KeY-Project.