public final class LoopContractInternalRule extends AbstractLoopContractRule
Rule for the application of LoopContract
s.
This splits the goal into two branches:
LoopContractInternalBuiltInRuleApp
AbstractLoopContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static LoopContractInternalRule |
INSTANCE
The only instance of this class.
|
private Term |
lastFocusTerm |
private AbstractAuxiliaryContractRule.Instantiation |
lastInstantiation |
private static Name |
NAME
This rule's name.
|
FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT
Modifier | Constructor and Description |
---|---|
private |
LoopContractInternalRule() |
contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, isApplicable
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
public static final LoopContractInternalRule INSTANCE
private static final Name NAME
private Term lastFocusTerm
getLastFocusTerm()
private AbstractAuxiliaryContractRule.Instantiation lastInstantiation
getLastInstantiation()
private static Term[] createPreconditions(Term selfTerm, LoopContract contract, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
selfTerm
- the self term.contract
- the loop contract being applied.heaps
- the heaps.localInVariables
- all free program variables in the block.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilder.services
- services.private static Term[] createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
localOutVariables
- all free program variables modified by the block.anonymisationHeaps
- the anonymization heaps.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilder.private static Term[] createPostconditionsNext(Term selfTerm, LoopContract contract, java.util.List<LocationVariable> heaps, AuxiliaryContract.Variables nextVariables, java.util.Map<LocationVariable,Term> modifiesClauses, Services services)
selfTerm
- the self term.contract
- the loop contract being applied.heaps
- the heaps.nextVariables
- the variables for the next loop iteration.modifiesClauses
- the modified clausesservices
- services.private static Term createContext(java.util.List<LocationVariable> heaps, AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder, AbstractAuxiliaryContractRule.Instantiation instantiation, Services services)
heaps
- the heaps.updatesBuilder
- an update builder.instantiation
- the instantiation for the current rule application.services
- services.private static Term[] createUsageAssumptions(Term[] postconditions, java.util.Map<LocationVariable,Function> anonOutHeaps, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
postconditions
- the postconditions.anonOutHeaps
- the heaps used in the anonOut update.localOutVariables
- all free program variables modified by the block.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilder.private static Term[] createUpdates(AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonOutHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder)
instantiation
- the instantiation.heaps
- the heaps.anonOutHeaps
- the heaps used in the anonOut update.modifiesClauses
- the modifies clauses.updatesBuilder
- an update builderprivate static AuxiliaryContract.Variables[] createVars(Goal goal, Term selfTerm, LoopContract contract, Services services)
goal
- the current goal.selfTerm
- the self term.contract
- the contract being applied.services
- services.private static void setUpGoals(Goal goal, ImmutableList<Goal> result, LoopContract contract, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.Map<LocationVariable,Function> anonOutHeaps, AuxiliaryContract.Variables[] vars, java.util.Map<LocationVariable,Term> modifiesClauses, Term[] assumptions, Term[] usageAssumptions, Term decreasesCheck, Term[] postconditions, Term[] postconditionsNext, Term[] updates, Term nextRemembranceUpdate, Term context, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services)
goal
- the current goal.result
- the next goals.contract
- the contract being applied.instantiation
- the instantiation.anonOutHeaps
- the heaps used in the anonOut update.vars
- the variables for both the current and the next loop iteration.modifiesClauses
- the modifies clauses.assumptions
- the preconditions for the validity branch.usageAssumptions
- the preconditions for the usage branch.decreasesCheck
- the decreases check.postconditions
- the postconditions for the current loop iteration.postconditionsNext
- the postconditions for the next loop iteration.updates
- the updates for the usage branch.nextRemembranceUpdate
- the remembrance update for the next loop iteration.context
- the update for the validity branch.configurator
- a configurator.services
- services.public Term getLastFocusTerm()
getLastFocusTerm
in class AbstractAuxiliaryContractRule
protected void setLastFocusTerm(Term lastFocusTerm)
setLastFocusTerm
in class AbstractAuxiliaryContractRule
lastFocusTerm
- the last focus term.AbstractAuxiliaryContractRule.getLastFocusTerm()
public AbstractAuxiliaryContractRule.Instantiation getLastInstantiation()
getLastInstantiation
in class AbstractAuxiliaryContractRule
protected void setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation)
setLastInstantiation
in class AbstractAuxiliaryContractRule
lastInstantiation
- the last instantiation.AbstractAuxiliaryContractRule.getLastInstantiation()
public LoopContractInternalBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices services)
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException