Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Field and Description |
---|---|
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> |
AbstractLoopInvariantRule.AdditionalHeapTerms.anonUpdateData |
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> |
AbstractLoopInvariantRule.LoopInvariantInformation.anonUpdateData
Anonymizing updates for all heaps.
|
Modifier and Type | Method and Description |
---|---|
protected static AbstractLoopInvariantRule.AnonUpdateData |
AbstractLoopInvariantRule.createAnonUpdate(LocationVariable heap,
Term mod,
LoopSpecification inv,
Services services)
Computes the anonymizing update, the loop heap, the base heap, and the
anonymized heap.
|
Constructor and Description |
---|
AdditionalHeapTerms(Term anonUpdate,
Term wellFormedAnon,
Term frameCondition,
Term reachableState,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData) |
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.