de.uka.ilkd.key.rule

Class AbstractLoopInvariantRule.LoopInvariantInformation

java.lang.Object

de.uka.ilkd.key.rule.AbstractLoopInvariantRule.LoopInvariantInformation

Enclosing class:

AbstractLoopInvariantRule

protected static class AbstractLoopInvariantRule.LoopInvariantInformation
extends java.lang.Object

A container object containing the information required for the concrete loop invariant rules to create the sequents for the new goals.

Field Summary

Fields

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 Summary

Constructors

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.

Method Summary

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

goal

public final Goal goal

The original goal.

services

public final Services services

The Services object.

inst

public final AbstractLoopInvariantRule.Instantiation inst

The AbstractLoopInvariantRule.Instantiation of parameters for the LoopScopeInvariantRule app.

ruleApp

public final LoopInvariantBuiltInRuleApp ruleApp

The RuleApp for this LoopScopeInvariantRule application.

goals

public final ImmutableList<Goal> goals

The goals created by the invariant rules application; those are filled with content by the concrete loop invariant rules.

termLabelState

public final TermLabelState termLabelState

The TermLabelState.

invTerm

public final Term invTerm

The loop invariant formula.

variantPO

public final Term variantPO

The proof obligation for the variant.

reachableState

public final Term reachableState

The reachable state formula.

anonUpdate

public final Term anonUpdate

The anonymized update Term.

wellFormedAnon

public final Term wellFormedAnon

The wellformed formula.

uAnonInv

public final Term uAnonInv

A formula containing the anonymized update and the loop invariant.

frameCondition

public final Term frameCondition

The frame condition.

uBeforeLoopDefAnonVariant

public final 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.

anonUpdateData

public final ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData

Anonymizing updates for all heaps.

Constructor Detail

LoopInvariantInformation

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)

Creates a new AbstractLoopInvariantRule.LoopInvariantInformation object.

Parameters:

goal - TODO

services - 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