de.uka.ilkd.key.rule

Class WhileInvariantRule.InfFlowData

java.lang.Object

de.uka.ilkd.key.rule.WhileInvariantRule.InfFlowData

Enclosing class:

WhileInvariantRule

private static final class WhileInvariantRule.InfFlowData
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
Term	applPredTerm
Term	guardAtPost
Term	guardAtPre
JavaBlock	guardJb
Term	guardTerm
Taclet	infFlowApp
ImmutableList<Term>	localOuts
ImmutableList<Term>	localOutsAtPost
ImmutableList<Term>	localOutsAtPre
ProofObligationVars	symbExecVars
Pair<Term,Term>	updates

Constructor Summary

Constructors

Modifier	Constructor and Description
private	InfFlowData(ProofObligationVars symbExecVars, Term guardAtPre, Term guardAtPost, JavaBlock guardJb, Term guardTerm, ImmutableList<Term> localOuts, ImmutableList<Term> localOutsAtPre, ImmutableList<Term> localOutsAtPost, Pair<Term,Term> updates, Term applPredTerm, Taclet infFlowApp)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

symbExecVars

public final ProofObligationVars symbExecVars

guardAtPre

public final Term guardAtPre

guardAtPost

public final Term guardAtPost

guardJb

public final JavaBlock guardJb

guardTerm

public final Term guardTerm

localOuts

public final ImmutableList<Term> localOuts

localOutsAtPre

public final ImmutableList<Term> localOutsAtPre

localOutsAtPost

public final ImmutableList<Term> localOutsAtPost

updates

public final Pair<Term,Term> updates

applPredTerm

public final Term applPredTerm

infFlowApp

public final Taclet infFlowApp

Constructor Detail

InfFlowData

private InfFlowData(ProofObligationVars symbExecVars,
                    Term guardAtPre,
                    Term guardAtPost,
                    JavaBlock guardJb,
                    Term guardTerm,
                    ImmutableList<Term> localOuts,
                    ImmutableList<Term> localOutsAtPre,
                    ImmutableList<Term> localOutsAtPost,
                    Pair<Term,Term> updates,
                    Term applPredTerm,
                    Taclet infFlowApp)