Package | Description |
---|---|
de.uka.ilkd.key.informationflow.proof.init | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
Modifier and Type | Method and Description |
---|---|
static StateVars |
StateVars.buildInfFlowPostVars(StateVars origPreVars,
StateVars origPostVars,
StateVars preVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildInfFlowPreVars(StateVars origPreVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
static StateVars |
StateVars.buildMethodContractPreVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Modifier and Type | Method and Description |
---|---|
static StateVars |
StateVars.buildInfFlowPostVars(StateVars origPreVars,
StateVars origPostVars,
StateVars preVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildInfFlowPreVars(StateVars origPreVars,
java.lang.String postfix,
Services services) |
static StateVars |
StateVars.buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Constructor and Description |
---|
StateVars(StateVars orig,
java.lang.String postfix,
Services services) |
Modifier and Type | Field and Description |
---|---|
StateVars |
ProofObligationVars.post
Variables for the pre and post condition.
|
StateVars |
ProofObligationVars.pre
Variables for the pre and post condition.
|
Constructor and Description |
---|
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) |
Copyright © 2003-2019 The KeY-Project.