Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Field and Description |
---|---|
AbstractLoopInvariantRule.Instantiation |
AbstractLoopInvariantRule.LoopInvariantInformation.inst
The
AbstractLoopInvariantRule.Instantiation of parameters for the
LoopScopeInvariantRule app. |
Modifier and Type | Method and Description |
---|---|
protected static AbstractLoopInvariantRule.Instantiation |
AbstractLoopInvariantRule.instantiate(LoopInvariantBuiltInRuleApp app,
Services services)
Constructs the
AbstractLoopInvariantRule.Instantiation object containing the relevant
parameters for this LoopScopeInvariantRule application. |
Modifier and Type | Method and Description |
---|---|
protected static Term |
AbstractLoopInvariantRule.conjunctFreeInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all free invariant formulas for the
LocationVariable s in heapContext. |
protected static Term |
AbstractLoopInvariantRule.conjunctInv(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.Map<LocationVariable,Term> atPres,
java.util.List<LocationVariable> heapContext)
Creates a conjunction of all invariant formulas for the
LocationVariable s in heapContext. |
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
protected static Pair<Term,Term> |
AbstractLoopInvariantRule.prepareVariant(AbstractLoopInvariantRule.Instantiation inst,
Term variant,
TermServices services)
Creates the variant proof obligation and update.
|
Constructor and Description |
---|
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
Copyright © 2003-2019 The KeY-Project.