public final class BlockContractInternalRule extends AbstractBlockContractRule
Rule for the application of BlockContract
s.
This splits the goal into two branches:
BlockContractInternalBuiltInRuleApp
AbstractBlockContractRule.BlockContractHint, AbstractBlockContractRule.InfFlowValidityData, AbstractBlockContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static BlockContractInternalRule |
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 |
BlockContractInternalRule() |
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.
|
BlockContractInternalBuiltInRuleApp |
createApp(PosInOccurrence occurrence,
TermServices services) |
private static Term[] |
createAssumptions(ImmutableSet<ProgramVariable> localOutVariables,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder) |
private static Term[] |
createPreconditions(BlockContract contract,
Term self,
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) |
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) |
private void |
setUpValidityGoal(ImmutableList<Goal> result,
boolean isInfFlow,
BlockContract contract,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation,
java.util.List<LocationVariable> heaps,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
AuxiliaryContract.Variables variables,
Term[] preconditions,
Term[] assumptions,
Term frameCondition,
Term[] updates,
AuxiliaryContractBuilders.GoalsConfigurator configurator,
AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
Services services)
Sets up the validity goal as the first goal in the list.
|
private static ImmutableList<Goal> |
splitIntoGoals(Goal goal,
BlockContract contract,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Term contextUpdate,
Term remembranceUpdate,
ImmutableSet<ProgramVariable> localOutVariables,
AuxiliaryContractBuilders.GoalsConfigurator configurator,
Services services) |
buildAfterVar, buildBodyPreservesSequent, buildInfFlowPostAssumption, buildInfFlowPreAssumption, buildLocalOutsAtPost, buildLocalOutsAtPre, contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, setUpInfFlowPartOfUsageGoal, setUpInfFlowValidityGoal
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
public static final BlockContractInternalRule INSTANCE
private static final Name NAME
private Term lastFocusTerm
getLastFocusTerm()
private AbstractAuxiliaryContractRule.Instantiation lastInstantiation
getLastInstantiation()
private static Term[] createPreconditions(BlockContract contract, Term self, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
contract
- the contract being applied.self
- the self term.heaps
- the heaps.localInVariables
- all free program variables in the block.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilder.services
- services.private static Term[] createAssumptions(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.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 modified clauses.services
- services.private static ImmutableList<Goal> splitIntoGoals(Goal goal, BlockContract contract, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, Term contextUpdate, Term remembranceUpdate, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services)
goal
- the current goal.contract
- the contract being applied.heaps
- the heaps.localInVariables
- all free program variables in the block.anonymisationHeaps
- the anonymization heaps.contextUpdate
- the context update.remembranceUpdate
- the remembrance update.localOutVariables
- all free program variables modified by the block.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 BlockContractInternalBuiltInRuleApp 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
public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractBlockContractRule
private void setUpValidityGoal(ImmutableList<Goal> result, boolean isInfFlow, BlockContract contract, BlockContractInternalBuiltInRuleApp application, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonymisationHeaps, ImmutableSet<ProgramVariable> localInVariables, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContract.Variables variables, Term[] preconditions, Term[] assumptions, Term frameCondition, Term[] updates, AuxiliaryContractBuilders.GoalsConfigurator configurator, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
result
- the new goals.isInfFlow
- whether or not this is an information flow proof.contract
- the block contract being applied.application
- the rule application.instantiation
- the instantiation.heaps
- the heaps.anonymisationHeaps
- the anonymization heaps.localInVariables
- all free program variables in the block.localOutVariables
- all free program variables modified by the block.variables
- the variables.preconditions
- the preconditions.assumptions
- the postconditions.frameCondition
- the framing condition.updates
- the updates.configurator
- a Configurator.conditionsAndClausesBuilder
- a ConditionsAndClausesBuilderservices
- services.