Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.taclettranslation.lemma |
Modifier and Type | Method and Description |
---|---|
void |
AbstractUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
Modifier and Type | Method and Description |
---|---|
void |
WindowUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
Modifier and Type | Method and Description |
---|---|
static IPersistablePO.LoadedPOContainer |
InfFlowContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Modifier and Type | Method and Description |
---|---|
static IPersistablePO.LoadedPOContainer |
DependencyContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalBlockContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
WellDefinednessPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalLoopContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
FunctionalOperationContractPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Modifier and Type | Method and Description |
---|---|
protected IPersistablePO.LoadedPOContainer |
AbstractProblemLoader.createProofObligationContainer()
Creates a
IPersistablePO.LoadedPOContainer if available which contains
the ProofOblInput for which a Proof should be instantiated. |
Modifier and Type | Method and Description |
---|---|
protected ProofAggregate |
AbstractProblemLoader.createProof(IPersistablePO.LoadedPOContainer poContainer)
Creates a
Proof for the given IPersistablePO.LoadedPOContainer and
tries to apply rules again. |
void |
ProblemLoaderControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result)
The loading has stopped.
|
protected void |
AbstractProblemLoader.loadSelectedProof(IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList)
Loads a proof from the proof list.
|
Modifier and Type | Method and Description |
---|---|
static IPersistablePO.LoadedPOContainer |
ProgramMethodPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
static IPersistablePO.LoadedPOContainer |
ProgramMethodSubsetPO.loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
Modifier and Type | Method and Description |
---|---|
static IPersistablePO.LoadedPOContainer |
TacletProofObligationInput.loadFrom(InitConfig initConfig,
java.util.Properties properties) |
Copyright © 2003-2019 The KeY-Project.