public abstract class AbstractAuxiliaryContractRule extends java.lang.Object implements BuiltInRule
Rule for the application of AuxiliaryContract
s.
AbstractAuxiliaryContractBuiltInRuleApp
Modifier and Type | Class and Description |
---|---|
static class |
AbstractAuxiliaryContractRule.Instantiation
This encapsulates all information from the rule application that is needed to apply the rule.
|
protected static class |
AbstractAuxiliaryContractRule.Instantiator
A builder for
AbstractAuxiliaryContractRule.Instantiation s. |
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
FULL_PRECONDITION_TERM_HINT |
static java.lang.String |
NEW_POSTCONDITION_TERM_HINT |
Constructor and Description |
---|
AbstractAuxiliaryContractRule() |
Modifier and Type | Method and Description |
---|---|
protected static Term |
createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services) |
protected static ProgramVariable |
createLocalVariable(java.lang.String nameBase,
KeYJavaType type,
Services services) |
java.lang.String |
displayName()
returns the display name of the rule
|
abstract Term |
getLastFocusTerm() |
abstract AbstractAuxiliaryContractRule.Instantiation |
getLastInstantiation() |
boolean |
isApplicableOnSubTerms() |
protected static boolean |
occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence) |
protected static void |
register(ProgramVariable pv,
Services services)
Adds
pv to the sevices ' program variable namespace. |
protected abstract void |
setLastFocusTerm(Term formula) |
protected abstract void |
setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation inst) |
java.lang.String |
toString() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
createApp, isApplicable
public static final java.lang.String FULL_PRECONDITION_TERM_HINT
public static final java.lang.String NEW_POSTCONDITION_TERM_HINT
protected static boolean occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence)
occurrence
- an occurrence.true
iff the occurrence is not at the top level in the succedent.protected static void register(ProgramVariable pv, Services services)
pv
to the sevices
' program variable namespace.pv
- a variable.services
- services.public abstract AbstractAuxiliaryContractRule.Instantiation getLastInstantiation()
public abstract Term getLastFocusTerm()
protected abstract void setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation inst)
inst
- the last instantiation.getLastInstantiation()
protected abstract void setLastFocusTerm(Term formula)
formula
- the last focus term.getLastFocusTerm()
public java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
protected static Term createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts, Services services)
localOuts
- a set of variables.services
- services.protected static ProgramVariable createLocalVariable(java.lang.String nameBase, KeYJavaType type, Services services)
nameBase
- a base name.type
- a type.services
- services.