All Methods Static Methods Instance Methods Concrete Methods
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.
|
(package private) static Pair<Term,Term> |
applyUpdates(Term focusTerm,
TermServices services) |
private Term |
bodyTerm(TermLabelState termLabelState,
Services services,
RuleApp ruleApp,
Sequent applicationSequent,
WhileInvariantRule.Instantiation inst,
Term invTerm,
Term frameCondition,
Term variantPO,
Goal bodyGoal,
JavaBlock guardJb,
Term guardTrueTerm) |
private static Term |
buildAfterVar(Term varTerm,
Services services) |
private static Term |
buildAtPostVar(Term varTerm,
java.lang.String suffix,
Services services) |
private static Term |
buildBeforeVar(Term varTerm,
Services services) |
private static ImmutableList<Term> |
buildLocalOutsAtPost(ImmutableList<Term> varTerms,
Services services) |
private static ImmutableList<Term> |
buildLocalOutsAtPre(ImmutableList<Term> varTerms,
Services services) |
(package private) static boolean |
checkApplicability(Goal g,
PosInOccurrence pio) |
private static boolean |
checkFocus(Term progPost) |
private Term |
conjunctFreeInv(Services services,
WhileInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext) |
private Term |
conjunctInv(Services services,
WhileInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext) |
private static WhileInvariantRule.AnonUpdateData |
createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services) |
LoopInvariantBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
private static Term |
createLocalAnonUpdate(ImmutableSet<ProgramVariable> localOuts,
Services services) |
java.lang.String |
displayName()
returns the display name of the rule
|
private SequentFormula |
initFormula(TermLabelState termLabelState,
WhileInvariantRule.Instantiation inst,
Term invTerm,
Term reachableState,
Services services,
Goal initGoal) |
private static WhileInvariantRule.Instantiation |
instantiate(LoopInvariantBuiltInRuleApp app,
Services services) |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
Name |
name()
the name of the rule
|
private void |
prepareBodyPreservesBranch(TermLabelState termLabelState,
Services services,
RuleApp ruleApp,
Sequent applicationSequent,
WhileInvariantRule.Instantiation inst,
Term invTerm,
Term wellFormedAnon,
Term frameCondition,
Term variantPO,
Goal bodyGoal,
JavaBlock guardJb,
Term guardTrueTerm,
Term[] uBeforeLoopDefAnonVariant,
Term uAnonInv) |
private Triple<JavaBlock,Term,Term> |
prepareGuard(WhileInvariantRule.Instantiation inst,
KeYJavaType booleanKJT,
LoopInvariantBuiltInRuleApp loopRuleApp,
TermServices services) |
private void |
prepareInvInitiallyValidBranch(TermLabelState termLabelState,
Services services,
RuleApp ruleApp,
WhileInvariantRule.Instantiation inst,
Term invTerm,
Term reachableState,
Goal initGoal) |
private static WhileInvariantRule.InfFlowData |
prepareSetUpOfInfFlowValidityGoal(WhileInvariantRule.AnonUpdateData anonUpdateData,
Term guardTerm,
WhileInvariantRule.Instantiation inst,
LoopSpecification spec,
Services services,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableSet<ProgramVariable> localIns,
ImmutableSet<ProgramVariable> localOuts,
Term anonUpdate,
JavaBlock guardJb) |
private void |
prepareUseCaseBranch(TermLabelState termLabelState,
Services services,
RuleApp ruleApp,
WhileInvariantRule.Instantiation inst,
Term wellFormedAnon,
Goal useGoal,
JavaBlock guardJb,
Term guardFalseTerm,
Term[] uAnon,
Term uAnonInv) |
private Pair<Term,Term> |
prepareVariant(WhileInvariantRule.Instantiation inst,
Term variant,
TermServices services) |
(package private) static void |
register(ProgramVariable pv,
Services services) |
private static void |
setUpInfFlowPartOfUseGoal(WhileInvariantRule.InfFlowData infData,
Term baseHeap,
Goal goal,
Services services) |
private static WhileInvariantRule.InfFlowData |
setUpInfFlowValidityGoal(Goal infFlowGoal,
LoopInvariantBuiltInRuleApp ruleApp,
WhileInvariantRule.Instantiation inst,
JavaBlock guardJb,
ImmutableSet<ProgramVariable> localIns,
ImmutableSet<ProgramVariable> localOuts,
ImmutableList<WhileInvariantRule.AnonUpdateData> anonUpdateDatas,
Term anonUpdate,
Services services) |
private void |
setupWdGoal(Goal goal,
LoopSpecification inv,
Term update,
Term selfTerm,
LocationVariable heap,
Term anonHeap,
Term localAnonUpdate,
ImmutableSet<ProgramVariable> localIns,
PosInOccurrence pio,
Services services) |
java.lang.String |
toString() |
private Term |
useCaseFormula(TermLabelState termLabelState,
Services services,
RuleApp ruleApp,
WhileInvariantRule.Instantiation inst,
Goal useGoal,
JavaBlock guardJb,
Term guardFalseTerm) |