private static final class WhileInvariantRule.InfFlowData
extends java.lang.Object
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 |
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) |
public final ProofObligationVars symbExecVars
public final Term guardAtPre
public final Term guardAtPost
public final JavaBlock guardJb
public final Term guardTerm
public final ImmutableList<Term> localOuts
public final ImmutableList<Term> localOutsAtPre
public final ImmutableList<Term> localOutsAtPost
public final Term applPredTerm
public final Taclet infFlowApp
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)