Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
protected abstract ProofEnvironment |
AbstractUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
ProofEnvironment |
DefaultUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
Proof.getEnv() |
Modifier and Type | Method and Description |
---|---|
void |
Proof.setEnv(ProofEnvironment env) |
void |
ProofAggregate.setProofEnv(ProofEnvironment env) |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
EnvNode.getProofEnv() |
ProofEnvironment |
ProofAggregateTask.getProofEnv() |
ProofEnvironment |
BasicTask.getProofEnv() |
ProofEnvironment |
TaskTreeNode.getProofEnv() |
ProofEnvironment |
ProofEnvironmentEvent.getSource() |
Constructor and Description |
---|
EnvNode(ProofEnvironment e) |
ProofEnvironmentEvent(ProofEnvironment source,
ProofOblInput po,
ProofAggregate proofList) |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
Modifier and Type | Method and Description |
---|---|
static ProofEnvironment |
SymbolicExecutionSideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
static ProofEnvironment |
SymbolicExecutionSideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
static ProofStarter |
SymbolicExecutionSideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof for the given
Sequent . |
Modifier and Type | Field and Description |
---|---|
protected ProofEnvironment |
TacletLoader.proofEnvironment |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
TacletLoader.getProofEnvForTaclets() |
Modifier and Type | Method and Description |
---|---|
void |
TacletSoundnessPOLoader.registerProofs(ProofAggregate aggregate,
ProofEnvironment proofEnv) |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
AbstractMediatorUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
Modifier and Type | Method and Description |
---|---|
static ProofEnvironment |
SideProofUtil.cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
Choice... enableChoices)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
Modifier and Type | Method and Description |
---|---|
static ProofStarter |
SideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
void |
ProofStarter.init(Sequent sequentToProve,
ProofEnvironment env,
java.lang.String proofName)
creates a new proof object for sequentToProve and registers it in the given environment
|
void |
ProofStarter.init(Term formulaToProve,
ProofEnvironment env)
creates a new proof object for formulaToProve and registers it in the given environment
|
Constructor and Description |
---|
UserProvidedInput(Sequent seq,
ProofEnvironment env) |
UserProvidedInput(Sequent seq,
ProofEnvironment env,
java.lang.String proofName) |
UserProvidedInput(Term formula,
ProofEnvironment env) |
Copyright © 2003-2019 The KeY-Project.