public abstract class AbstractBlockContractRule extends AbstractAuxiliaryContractRule
Rule for the application of BlockContract
s.
AbstractBlockContractBuiltInRuleApp
Modifier and Type | Class and Description |
---|---|
static class |
AbstractBlockContractRule.BlockContractHint |
protected static class |
AbstractBlockContractRule.InfFlowValidityData |
protected static class |
AbstractBlockContractRule.Instantiator
A builder for
Instantiation s. |
AbstractAuxiliaryContractRule.Instantiation
FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT
Constructor and Description |
---|
AbstractBlockContractRule() |
createLocalAnonUpdate, createLocalVariable, displayName, getLastFocusTerm, getLastInstantiation, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, setLastFocusTerm, setLastInstantiation, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
createApp, getOrigin
public static ImmutableSet<BlockContract> getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation, Goal goal, Services services)
instantiation
- an instantiation.goal
- the current goal.services
- services.public static ImmutableSet<BlockContract> getApplicableContracts(SpecificationRepository specifications, JavaStatement statement, Modality modality, Goal goal)
specifications
- a specification repository.statement
- a block.modality
- the current goal's modality.goal
- the current goal.protected static ImmutableSet<BlockContract> filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts, Goal goal)
collectedContracts
- a set of block contracts.goal
- the current goal.protected static boolean contractApplied(BlockContract contract, Goal goal)
contract
- a block contract.goal
- the current goal.true
if the contract has already been applied.protected static java.util.Map<LocationVariable,Function> createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables, BlockContract contract, TermServices services)
variables
- variables.contract
- a block contract.services
- services.protected static Term buildAfterVar(Term varTerm, java.lang.String suffix, Services services)
protected static ImmutableList<Term> buildLocalOutsAtPre(ImmutableList<Term> varTerms, Services services)
protected static ImmutableList<Term> buildLocalOutsAtPost(ImmutableList<Term> varTerms, Services services)
protected static Term buildInfFlowPreAssumption(ProofObligationVars instVars, ImmutableList<Term> localOuts, ImmutableList<Term> localOutsAtPre, Term baseHeap, TermBuilder tb)
protected static Term buildInfFlowPostAssumption(ProofObligationVars instVars, ImmutableList<Term> localOuts, ImmutableList<Term> localOutsAtPost, Term baseHeap, Term applPredTerm, TermBuilder tb)
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 void setUpInfFlowPartOfUsageGoal(Goal usageGoal, AbstractBlockContractRule.InfFlowValidityData infFlowValitidyData, Term contextUpdate, Term remembranceUpdate, Term anonymisationUpdate, TermBuilder tb)
protected AbstractBlockContractRule.InfFlowValidityData setUpInfFlowValidityGoal(Goal infFlowGoal, BlockContract contract, java.util.Map<LocationVariable,Function> anonymisationHeaps, Services services, AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, ImmutableSet<ProgramVariable> localOutVariables, BlockContractInternalBuiltInRuleApp application, AbstractAuxiliaryContractRule.Instantiation instantiation)
Copyright © 2003-2019 The KeY-Project.