protected static class AbstractLoopInvariantRule.LoopInvariantInformation
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
Term |
anonUpdate
The anonymized update
Term . |
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> |
anonUpdateData
Anonymizing updates for all heaps.
|
Term |
frameCondition
The frame condition.
|
Goal |
goal
The original goal.
|
ImmutableList<Goal> |
goals
The goals created by the invariant rules application; those are
filled with content by the concrete loop invariant rules.
|
AbstractLoopInvariantRule.Instantiation |
inst
The
AbstractLoopInvariantRule.Instantiation of parameters for the
LoopScopeInvariantRule app. |
Term |
invTerm
The loop invariant formula.
|
Term |
reachableState
The reachable state formula.
|
LoopInvariantBuiltInRuleApp |
ruleApp
The
RuleApp for this LoopScopeInvariantRule
application. |
Services |
services
The
Services object. |
TermLabelState |
termLabelState
The
TermLabelState . |
Term |
uAnonInv
A formula containing the anonymized update and the loop invariant.
|
Term[] |
uBeforeLoopDefAnonVariant
An array containing the original update, the "before the loop" update
for reasoning about the variant, the anonymized update, and the
variant update.
|
Term |
variantPO
The proof obligation for the variant.
|
Term |
wellFormedAnon
The wellformed formula.
|
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. |
public final Goal goal
public final AbstractLoopInvariantRule.Instantiation inst
AbstractLoopInvariantRule.Instantiation
of parameters for the
LoopScopeInvariantRule
app.public final LoopInvariantBuiltInRuleApp ruleApp
RuleApp
for this LoopScopeInvariantRule
application.public final ImmutableList<Goal> goals
public final TermLabelState termLabelState
TermLabelState
.public final Term invTerm
public final Term variantPO
public final Term reachableState
public final Term wellFormedAnon
public final Term uAnonInv
public final Term frameCondition
public final Term[] uBeforeLoopDefAnonVariant
public final ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData
public 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)
AbstractLoopInvariantRule.LoopInvariantInformation
object.goal
- TODOservices
- The Services
object.inst
- The AbstractLoopInvariantRule.Instantiation
of parameters for the
LoopScopeInvariantRule
app.ruleApp
- The RuleApp
for this
LoopScopeInvariantRule
application.goals
- The goals created by the invariant rules application;
those are filled with content by the concrete loop
invariant rules.termLabelState
- The TermLabelState
.invTerm
- The loop invariant formula.variantPO
- The proof obligation for the variant.reachableState
- The reachable state formula.anonUpdate
- The anonymized update Term
.wellFormedAnon
- The wellformed formula.uAnonInv
- A formula containing the anonymized update and the loop
invariant.frameCondition
- The frame condition.uBeforeLoopDefAnonVariant
- An array containing the original update, the "before the
loop" update for reasoning about the variant, the
anonymized update, and the variant update.anonUpdateData
- TODO