All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private ImmutableList<Goal> |
apply(Goal goal,
Services services,
BlockContractBuiltInRuleApp application) |
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp application)
the rule is applied on the given goal using the
information of rule application.
|
private static Term |
buildAfterVar(Term varTerm,
String suffix,
Services services) |
(package private) static SequentFormula |
buildBodyPreservesSequent(InfFlowPOSnippetFactory f,
InfFlowProof proof) |
private static Term |
buildInfFlowPostAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPost,
Term baseHeap,
Term applPredTerm,
TermBuilder tb) |
private static Term |
buildInfFlowPreAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPre,
Term baseHeap,
TermBuilder tb) |
private static ImmutableList<Term> |
buildLocalOutsAtPost(ImmutableList<Term> varTerms,
Services services) |
private static ImmutableList<Term> |
buildLocalOutsAtPre(ImmutableList<Term> varTerms,
Services services) |
private static boolean |
contractApplied(BlockContract contract,
Goal goal) |
private Map<LocationVariable,Function> |
createAndRegisterAnonymisationVariables(Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
BlockContractBuiltInRuleApp |
createApp(PosInOccurrence occurrence,
TermServices services) |
private ProgramVariable |
createLocalVariable(String nameBase,
KeYJavaType type,
Services services) |
String |
displayName()
returns the display name of the rule
|
private static ImmutableSet<BlockContract> |
filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
static ImmutableSet<BlockContract> |
getApplicableContracts(BlockContractRule.Instantiation instantiation,
Goal goal,
Services services) |
private static ImmutableSet<BlockContract> |
getApplicableContracts(SpecificationRepository specifications,
StatementBlock block,
Modality modality,
Goal goal) |
static BlockContractRule.Instantiation |
instantiate(Term formula,
Goal goal,
Services services) |
boolean |
isApplicable(Goal goal,
PosInOccurrence occurrence)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
Name |
name()
the name of the rule
|
private static boolean |
occursNotAtTopLevelInSuccedent(PosInOccurrence occurrence) |
(package private) static void |
register(ProgramVariable pv,
Services services) |
private void |
setUpInfFlowPartOfUsageGoal(Goal usageGoal,
BlockContractRule.InfFlowValidityData infFlowValitidyData,
Term contextUpdate,
Term remembranceUpdate,
Term anonymisationUpdate,
TermBuilder tb) |
private BlockContractRule.InfFlowValidityData |
setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
Map<LocationVariable,Function> anonymisationHeaps,
Services services,
BlockContract.Variables variables,
ProgramVariable exceptionParameter,
List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractBuiltInRuleApp application,
BlockContractRule.Instantiation instantiation) |
String |
toString() |