public abstract class KeYApi
extends java.lang.Object
This facility is the entry point to the different KeY apis.
Currently it support the bootstrapping of the KeYEnvironment
and the loading of proofs.
Created at 6.4.17
ProofScriptCommandApi
Modifier and Type | Method and Description |
---|---|
static ProofMacroApi |
getMacroApi() |
static ProofScriptCommandApi |
getScriptCommandApi() |
static java.lang.String |
getVersion() |
static ProofManagementApi |
loadFromKeyFile(java.io.File keyFile) |
static ProofManagementApi |
loadProof(java.io.File javaSourceCode) |
static ProofManagementApi |
loadProof(java.io.File location,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes) |
abstract void |
loadProofFile(java.io.File file,
java.util.List<java.io.File> classPaths,
java.io.File bootClassPath,
java.util.List<java.io.File> includes)
Load a proof file, creates a KeY environment that can be accessed with other methods from this facade
|
public static java.lang.String getVersion()
public static ProofScriptCommandApi getScriptCommandApi()
public static ProofMacroApi getMacroApi()
public static ProofManagementApi loadFromKeyFile(java.io.File keyFile) throws ProblemLoaderException
keyFile
- ProblemLoaderException
public static ProofManagementApi loadProof(java.io.File location, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes) throws ProblemLoaderException
location
- classPath
- bootClassPath
- includes
- ProblemLoaderException
public static ProofManagementApi loadProof(java.io.File javaSourceCode) throws ProblemLoaderException
javaSourceCode
- ProblemLoaderException
public abstract void loadProofFile(java.io.File file, java.util.List<java.io.File> classPaths, java.io.File bootClassPath, java.util.List<java.io.File> includes)
file
- Path to the source code folder/file or to a *.proof fileclassPaths
- Optionally: Additional specifications for API classesbootClassPath
- Optionally: Different default specifications for Java APIincludes
- Optionally: Additional includes to considerCopyright © 2003-2019 The KeY-Project.