de.uka.ilkd.key.api

Class KeYApi

java.lang.Object

de.uka.ilkd.key.api.KeYApi

public abstract class KeYApi
extends java.lang.Object

The Entry Point.

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

Author:

Sarah Grebing, Alexander Weigl

See Also:

ProofScriptCommandApi

Field Summary

Fields

Modifier and Type	Field and Description
private static ProofMacroApi	proofMacroApi
private static ProofScriptCommandApi	scriptCommandApi

Constructor Summary

Constructors

Modifier	Constructor and Description
private	KeYApi() Create a new KeY API and create the sub APIs

Method Summary

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

proofMacroApi

private static final ProofMacroApi proofMacroApi

scriptCommandApi

private static final ProofScriptCommandApi scriptCommandApi

Constructor Detail

KeYApi

private KeYApi()

Create a new KeY API and create the sub APIs

Method Detail

getVersion

public static java.lang.String getVersion()

Returns:

getScriptCommandApi

public static ProofScriptCommandApi getScriptCommandApi()

Returns:

non-null

getMacroApi

public static ProofMacroApi getMacroApi()

Returns:

a non-null references to the macro api

loadFromKeyFile

public static ProofManagementApi loadFromKeyFile(java.io.File keyFile)
                                          throws ProblemLoaderException

Parameters:

keyFile -

Returns:

Throws:

ProblemLoaderException

loadProof

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

Parameters:

location -

classPath -

bootClassPath -

includes -

Returns:

Throws:

ProblemLoaderException

loadProof

public static ProofManagementApi loadProof(java.io.File javaSourceCode)
                                    throws ProblemLoaderException

Parameters:

javaSourceCode -

Returns:

Throws:

ProblemLoaderException

loadProofFile

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)

Load a proof file, creates a KeY environment that can be accessed with other methods from this facade

Parameters:

file - Path to the source code folder/file or to a *.proof file

classPaths - Optionally: Additional specifications for API classes

bootClassPath - Optionally: Different default specifications for Java API

includes - Optionally: Additional includes to consider