Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.symbolic_execution.model.impl | |
org.key_project.ui.interactionlog.model.builtin |
Modifier and Type | Field and Description |
---|---|
LoopInvariantBuiltInRuleApp |
AbstractLoopInvariantRule.LoopInvariantInformation.ruleApp
The
RuleApp for this LoopScopeInvariantRule
application. |
Modifier and Type | Method and Description |
---|---|
LoopInvariantBuiltInRuleApp |
WhileInvariantRule.createApp(PosInOccurrence pos,
TermServices services) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.replacePos(PosInOccurrence newPos) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.setIfInsts(ImmutableList<PosInOccurrence> ifInsts) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.setLoopInvariant(LoopSpecification inv) |
LoopInvariantBuiltInRuleApp |
LoopInvariantBuiltInRuleApp.tryToInstantiate(Goal goal) |
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. |
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. |
Modifier and Type | Method and Description |
---|---|
LoopInvariantBuiltInRuleApp |
ExecutionLoopInvariant.getAppliedRuleApp()
Returns the applied
RuleApp . |
Constructor and Description |
---|
LoopInvariantBuiltInRuleInteraction(LoopInvariantBuiltInRuleApp app,
Node node) |
Copyright © 2003-2019 The KeY-Project.