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.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.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.proof.mgt |
This package contains classes for proof environments and proof management.
|
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
|
void |
AbstractUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
void |
AbstractUserInterfaceControl.proofCreated(ProblemInitializer sender,
ProofAggregate proofAggregate) |
void |
UserInterfaceControl.registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
void |
DefaultUserInterfaceControl.registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
Modifier and Type | Method and Description |
---|---|
void |
MainWindow.addProblem(ProofAggregate plist) |
void |
TaskTree.addProof(ProofAggregate plist) |
void |
WindowUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
void |
WindowUserInterfaceControl.registerProofAggregate(ProofAggregate pa) |
Modifier and Type | Class and Description |
---|---|
class |
CompoundProof |
class |
SingleProof |
Modifier and Type | Method and Description |
---|---|
static ProofAggregate |
ProofAggregate.createProofAggregate(Proof[] proofs,
java.lang.String name) |
static ProofAggregate |
ProofAggregate.createProofAggregate(ProofAggregate[] proofs,
java.lang.String name) |
static ProofAggregate |
ProofAggregate.createProofAggregate(Proof proof,
java.lang.String name) |
ProofAggregate |
CompoundProof.get(int i) |
ProofAggregate |
SingleProof.getChildrenAt(int i) |
ProofAggregate |
CompoundProof.getChildrenAt(int i) |
abstract ProofAggregate |
ProofAggregate.getChildrenAt(int i) |
Modifier and Type | Method and Description |
---|---|
java.util.List<ProofAggregate> |
SingleProof.getChildren() |
java.util.List<ProofAggregate> |
CompoundProof.getChildren() |
abstract java.util.List<ProofAggregate> |
ProofAggregate.getChildren() |
Modifier and Type | Method and Description |
---|---|
static ProofAggregate |
ProofAggregate.createProofAggregate(ProofAggregate[] proofs,
java.lang.String name) |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
KeYUserProblemFile.getPO() |
ProofAggregate |
ProofOblInput.getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
ProofAggregate |
AbstractPO.getPO() |
ProofAggregate |
ProblemInitializer.startProver(EnvInput envInput,
ProofOblInput po) |
ProofAggregate |
ProblemInitializer.startProver(InitConfig initConfig,
ProofOblInput po) |
Modifier and Type | Method and Description |
---|---|
void |
ProblemInitializer.ProblemInitializerListener.proofCreated(ProblemInitializer sender,
ProofAggregate proofAggregate) |
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. |
Modifier and Type | Method and Description |
---|---|
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 |
---|---|
ProofAggregate |
ProofEnvironmentEvent.getProofList() |
ProofAggregate |
ProofAggregateTask.getProofList() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<ProofAggregate> |
ProofEnvironment.getProofs()
retrieves all proofs registered at this environment
|
Modifier and Type | Method and Description |
---|---|
TaskTreeNode |
TaskTreeModel.addProof(ProofAggregate plist) |
void |
ProofEnvironment.registerProof(ProofOblInput po,
ProofAggregate pl)
registers a proof loaded with the given
ProofOblInput . |
void |
ProofEnvironment.removeProofList(ProofAggregate pl) |
Constructor and Description |
---|
BasicTask(ProofAggregate pl)
creates a task with a single proof.
|
ProofAggregateTask(ProofAggregate ps) |
ProofEnvironmentEvent(ProofEnvironment source,
ProofOblInput po,
ProofAggregate proofList) |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
ProofObligationCreator.create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
ProofAggregate |
TacletProofObligationInput.getPO() |
ProofAggregate |
TacletSoundnessPOLoader.getResultingProof() |
Modifier and Type | Method and Description |
---|---|
void |
TacletSoundnessPOLoader.registerProofs(ProofAggregate aggregate,
ProofEnvironment proofEnv) |
void |
TacletSoundnessPOLoader.LoaderListener.stopped(ProofAggregate p,
ImmutableSet<Taclet> taclets,
boolean addAsAxioms) |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
AbstractMediatorUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
void |
ConsoleUserInterfaceControl.registerProofAggregate(ProofAggregate pa) |
void |
AbstractMediatorUserInterfaceControl.registerProofAggregate(ProofAggregate pa)
Registers an already created
ProofAggregate in this UserInterfaceControl . |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
ProofStarter.UserProvidedInput.getPO() |
ProofAggregate |
HelperClassForTests.parse(java.io.File file) |
ProofAggregate |
HelperClassForTests.parse(java.io.File file,
Profile profile) |
ProofAggregate |
HelperClassForTests.parseThrowException(java.io.File file) |
ProofAggregate |
HelperClassForTests.parseThrowException(java.io.File file,
Profile profile) |
Copyright © 2003-2019 The KeY-Project.