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.gui.testgen |
This package contains the graphical user interface of the test generation backend.
|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.smt.counterexample | |
de.uka.ilkd.key.smt.testgen | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.ui |
Modifier and Type | Class and Description |
---|---|
class |
KeYEnvironment<U extends UserInterfaceControl>
Instances of this class are used to collect and access all
relevant information for verification with KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractUserInterfaceControl
Provides a basic implementation of
UserInterfaceControl . |
class |
DefaultUserInterfaceControl
The
DefaultUserInterfaceControl which allows proving in case
that no specific user interface is available. |
Constructor and Description |
---|
DefaultProofControl(UserInterfaceControl ui,
DefaultUserInterfaceControl defaultProverTaskListener)
Constructor.
|
DefaultProofControl(UserInterfaceControl ui,
DefaultUserInterfaceControl defaultProverTaskListener,
RuleCompletionHandler ruleCompletionHandler)
Constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
WindowUserInterfaceControl
Implementation of
UserInterfaceControl which controls the MainWindow
with the typical user interface of KeY. |
Modifier and Type | Method and Description |
---|---|
protected Proof |
CounterExampleAction.MainWindowCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected void |
CounterExampleAction.MainWindowCounterExampleGenerator.semanticsBlastingCompleted(UserInterfaceControl ui)
This method is called after the
SemanticsBlastingMacro has been executed. |
Modifier and Type | Method and Description |
---|---|
protected abstract Proof |
AbstractCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected Proof |
AbstractSideProofCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
void |
AbstractCounterExampleGenerator.searchCounterExample(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent)
Searches a counter example for the given
Sequent . |
protected void |
AbstractCounterExampleGenerator.semanticsBlastingCompleted(UserInterfaceControl ui)
This method is called after the
SemanticsBlastingMacro has been executed. |
Modifier and Type | Method and Description |
---|---|
protected UserInterfaceControl |
AbstractTestGenerator.getUI() |
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractTestGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
protected void |
AbstractTestGenerator.handleAllProofsPerformed(UserInterfaceControl ui) |
protected void |
AbstractTestGenerator.selectProof(UserInterfaceControl ui,
Proof proof) |
Constructor and Description |
---|
AbstractTestGenerator(UserInterfaceControl ui,
Proof originalProof)
Constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
SymbolicExecutionEnvironment<U extends UserInterfaceControl>
Instances of this class are used to collect and access all
relevant information for symbolic execution tree extraction of
Proof s
via an SymbolicExecutionTreeBuilder . |
Modifier and Type | Class and Description |
---|---|
class |
AbstractMediatorUserInterfaceControl
Provides a basic implementation of
UserInterfaceControl for
user interfaces in which a KeYMediator is available. |
class |
ConsoleUserInterfaceControl
Implementation of
UserInterfaceControl used by command line interface of KeY. |
Copyright © 2003-2019 The KeY-Project.