public abstract class AbstractLoopContractRule extends AbstractAuxiliaryContractRule
Rule for the application of LoopContract
s.
AbstractLoopContractBuiltInRuleApp
Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractLoopContractRule.Instantiator
A builder for
Instantiation s. |
AbstractAuxiliaryContractRule.Instantiation
FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT
Constructor and Description |
---|
AbstractLoopContractRule() |
createLocalAnonUpdate, createLocalVariable, displayName, getLastFocusTerm, getLastInstantiation, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, setLastFocusTerm, setLastInstantiation, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
createApp
public static ImmutableSet<LoopContract> getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation, Goal goal, Services services)
instantiation
- an instantiation.goal
- the current goal.services
- services.public static ImmutableSet<LoopContract> getApplicableContracts(SpecificationRepository specifications, JavaStatement statement, Modality modality, Goal goal)
specifications
- a specification repository.statement
- a statement.modality
- the current goal's modality.goal
- the current goal.protected static ImmutableSet<LoopContract> filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts, Goal goal)
collectedContracts
- a set of loop contracts.goal
- the current goal.protected static boolean contractApplied(LoopContract contract, Goal goal)
contract
- a loop contract.goal
- the current goal.true
if the contract has already been applied.public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
public AbstractAuxiliaryContractRule.Instantiation instantiate(Term formula, Goal goal, Services services)
formula
- the formula on which the rule is to be applied.goal
- the current goal.services
- services.protected java.util.Map<LocationVariable,Function> createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables, LoopContract contract, TermServices services)
variables
- variables.contract
- a loop contract.services
- services.