public final class BlockContractExternalRule extends AbstractBlockContractRule
Rule for the application of BlockContract
s.
This splits the goal into two branches:
The validity of all BlockContract
s that were used in the application of this rule must be
proven in a FunctionalBlockContractPO
before the current proof is considered closed.
BlockContractExternalBuiltInRuleApp
AbstractBlockContractRule.BlockContractHint, AbstractBlockContractRule.InfFlowValidityData, AbstractBlockContractRule.Instantiator
AbstractAuxiliaryContractRule.Instantiation
Modifier and Type | Field and Description |
---|---|
static BlockContractExternalRule |
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 |
BlockContractExternalRule() |
buildAfterVar, buildBodyPreservesSequent, buildInfFlowPostAssumption, buildInfFlowPreAssumption, buildLocalOutsAtPost, buildLocalOutsAtPre, contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, setUpInfFlowPartOfUsageGoal, setUpInfFlowValidityGoal
createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString
public static final BlockContractExternalRule INSTANCE
private static final Name NAME
private Term lastFocusTerm
getLastFocusTerm()
private AbstractAuxiliaryContractRule.Instantiation lastInstantiation
getLastInstantiation()
private static Term[] createPreconditions(AbstractAuxiliaryContractRule.Instantiation instantiation, BlockContract contract, 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, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
contextUpdate
- the context update.heaps
- the heaps.anonymisationHeaps
- the anonymization heaps.variables
- the variables.modifiesClauses
- the modified clauses.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 IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
public boolean isApplicable(Goal goal, PosInOccurrence occurrence)
BuiltInRule
isApplicable
in interface BuiltInRule
isApplicable
in class AbstractBlockContractRule
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