public class ProofObligationVars
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
Term |
exceptionParameter
Exception Variable for the try-catch statement.
|
ImmutableList<Term> |
formalParams
The formal parameters of a method.
|
StateVars |
post
Variables for the pre and post condition.
|
java.lang.String |
postfix
If this object was created form another ProofObligationVars
object by adding a postfix to the variable names, then this
variable contains the used postfix.
|
StateVars |
pre
Variables for the pre and post condition.
|
Constructor and Description |
---|
ProofObligationVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
ProofObligationVars(ProofObligationVars orig,
java.lang.String postfix,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
ProofObligationVars |
labelHeapAtPreAsAnonHeapFunc() |
public final StateVars pre
public final StateVars post
public final Term exceptionParameter
public final ImmutableList<Term> formalParams
public final java.lang.String postfix
public ProofObligationVars(IProgramMethod pm, KeYJavaType kjt, Services services)
public ProofObligationVars(ProofObligationVars orig, java.lang.String postfix, Services services)
public ProofObligationVars(StateVars pre, StateVars post, Term exceptionParameter, ImmutableList<Term> formalParams, Services services)
public ProofObligationVars(StateVars pre, StateVars post, Term exceptionParameter, ImmutableList<Term> formalParams, TermBuilder tb)
public ProofObligationVars labelHeapAtPreAsAnonHeapFunc()
Copyright © 2003-2019 The KeY-Project.