Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
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.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
static ProofManagementApi |
KeYApi.loadFromKeyFile(java.io.File keyFile) |
static ProofManagementApi |
KeYApi.loadProof(java.io.File javaSourceCode) |
static ProofManagementApi |
KeYApi.loadProof(java.io.File location,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes) |
Modifier and Type | Method and Description |
---|---|
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(java.io.File keyFile) |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes)
Loads the given location and returns all required references as
KeYEnvironment . |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
RuleCompletionHandler ruleCompletionHandler)
Loads the given location and returns all required references as
KeYEnvironment . |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
AbstractProblemLoader |
AbstractUserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
AbstractProblemLoader |
UserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
static KeYEnvironment<DefaultUserInterfaceControl> |
KeYEnvironment.load(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
RuleCompletionHandler ruleCompletionHandler,
boolean forceNewProfileOfNewProofs)
Loads the given location and returns all required references as
KeYEnvironment . |
void |
AbstractUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
Modifier and Type | Method and Description |
---|---|
AbstractProblemLoader |
WindowUserInterfaceControl.load(Profile profile,
java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
java.util.Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs)
Opens a java file in this
UserInterfaceControl and returns the instantiated AbstractProblemLoader
which can be used to instantiated proofs programmatically. |
void |
WindowUserInterfaceControl.loadingFinished(AbstractProblemLoader loader,
IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList,
AbstractProblemLoader.ReplayResult result) |
static KeYEnvironment<WindowUserInterfaceControl> |
WindowUserInterfaceControl.loadInMainWindow(Profile profile,
java.io.File location,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes,
boolean forceNewProfileOfNewProofs,
boolean makeMainWindowVisible)
Loads the given location and returns all required references as
KeYEnvironment
with KeY's MainWindow . |
Modifier and Type | Method and Description |
---|---|
protected ProblemLoaderException |
AbstractProblemLoader.recoverParserErrorMessage(java.lang.Exception e)
Tries to recover parser errors and make them human-readable,
rewrap them into ProblemLoaderExceptions.
|
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.String,Location> |
AbstractProblemLoader.getProofScript() |
void |
AbstractProblemLoader.load()
Executes the loading process and tries to instantiate a proof
and to re-apply rules on it if possible.
|
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 KeYEnvironment<DefaultUserInterfaceControl> |
HelperClassForTests.createKeYEnvironment() |
static java.util.HashMap<java.lang.String,java.lang.String> |
HelperClassForTests.setDefaultTacletOptions(java.io.File baseDir,
java.lang.String javaPathInBaseDir)
Ensures that the default taclet options are defined.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
HelperClassForTests.setDefaultTacletOptionsForTarget(java.io.File javaFile,
java.lang.String containerTypeName,
java.lang.String targetName)
Ensures that the default taclet options are defined.
|
Copyright © 2003-2019 The KeY-Project.