public final class LoopContractExternalRule extends AbstractLoopContractRule
Rule for the application of LoopContract
s.
This splits the goal into two branches:
The validity of all LoopContract
s that were used in the application of this rule must be
proven in a FunctionalLoopContractPO
before the current proof is considered closed.
LoopContractExternalBuiltInRuleApp
AbstractLoopContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static LoopContractExternalRule |
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 |
LoopContractExternalRule() |
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.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
private static Term[] |
createPreconditions(Term selfTerm,
LoopContract contract,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
Services services) |
private static Term[] |
createUpdates(Term contextUpdate,
java.util.List<LocationVariable> heaps,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> modifiesClauses,
Services services) |
private static Term[] |
createUsageAssumptions(ImmutableSet<ProgramVariable> localOutVariables,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder) |
Term |
getLastFocusTerm() |
AbstractAuxiliaryContractRule.Instantiation |
getLastInstantiation() |
boolean |
isApplicable(Goal goal,
PosInOccurrence occurrence)
returns true iff a rule is applicable at the given
position.
|
Name |
name()
the name of the rule
|
protected void |
setLastFocusTerm(Term lastFocusTerm) |
protected void |
setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation) |
contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
public static final LoopContractExternalRule INSTANCE
private static final Name NAME
private Term lastFocusTerm
getLastFocusTerm()
private AbstractAuxiliaryContractRule.Instantiation lastInstantiation
getLastInstantiation()
private static Term[] createUpdates(Term contextUpdate, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContract.Variables variables, java.util.Map<LocationVariable,Term> modifiesClauses, Services services)
contextUpdate
- the context update.heaps
- the heaps.anonymisationHeaps
- the anonymization heaps.variables
- the variables.modifiesClauses
- the modifies clauses.services
- services.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[] createUsageAssumptions(ImmutableSet<ProgramVariable> localOutVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
localOutVariables
- all free program variables modified by the block.anonymisationHeaps
- the anonymization heaps.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilder.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 IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractLoopContractRule
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