de.uka.ilkd.key.rule

Class AbstractLoopInvariantRule.AdditionalHeapTerms

java.lang.Object

de.uka.ilkd.key.rule.AbstractLoopInvariantRule.AdditionalHeapTerms

Enclosing class:

AbstractLoopInvariantRule

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

A container with data for the additional terms with assertions about the heap; that is, the anonymizing update, the wellformed term, the frame condition and the reachable state formula.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
Term	anonUpdate
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData>	anonUpdateData
Term	frameCondition
Term	reachableState
Term	wellFormedAnon

Constructor Summary

Constructors

Constructor and Description
AdditionalHeapTerms(Term anonUpdate, Term wellFormedAnon, Term frameCondition, Term reachableState, ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

anonUpdate

public final Term anonUpdate

wellFormedAnon

public final Term wellFormedAnon

frameCondition

public final Term frameCondition

reachableState

public final Term reachableState

anonUpdateData

public final ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData

Constructor Detail

AdditionalHeapTerms

public AdditionalHeapTerms(Term anonUpdate,
                           Term wellFormedAnon,
                           Term frameCondition,
                           Term reachableState,
                           ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)