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
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)
static SequentFormula buildBodyPreservesSequent(InfFlowPOSnippetFactory f, InfFlowProof proof)
private static ProofObligationVars generateProofObligationVariables(AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, LocationVariable baseHeap, ImmutableList<Term> localVarsAtPre, ImmutableList<Term> localVarsAtPost, Services services, TermBuilder tb)
private static void addProofObligation(Goal infFlowGoal, InfFlowProof proof, BlockContract contract, IFProofObligationVars ifVars, ExecutionContext ec, Services services)
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)