de.uka.ilkd.key.control

Class KeYEnvironment<U extends UserInterfaceControl>

java.lang.Object

de.uka.ilkd.key.control.KeYEnvironment<U>

Direct Known Subclasses:

SymbolicExecutionEnvironment

public class KeYEnvironment<U extends UserInterfaceControl>
extends java.lang.Object

Instances of this class are used to collect and access all relevant information for verification with KeY.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	disposed Indicates that this KeYEnvironment is disposed.
private InitConfig	initConfig The loaded project.
private Proof	loadedProof An optional Proof which was loaded by the specified proof file.
private Pair<java.lang.String,Location>	proofScript An optional field denoting a script contained in the proof file.
private AbstractProblemLoader.ReplayResult	replayResult The AbstractProblemLoader.ReplayResult if available.
private U	ui The UserInterfaceControl in which the Proof is loaded.

Constructor Summary

Constructors

Constructor and Description
KeYEnvironment(U ui, InitConfig initConfig) Constructor
KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, Pair<java.lang.String,Location> proofScript, AbstractProblemLoader.ReplayResult replayResult) Constructor

Method Summary

Modifier and Type	Method and Description
Proof	createProof(ProofOblInput input) Creates a new Proof with help of the UserInterfaceControl.
void	dispose() Disposes this KeYEnvironment.
InitConfig	getInitConfig() Returns the loaded project.
JavaInfo	getJavaInfo() Returns the used JavaInfo.
Proof	getLoadedProof() Returns the loaded Proof if a proof file was loaded.
Profile	getProfile()
ProofControl	getProofControl() Returns the ProofControl of getUi().
Pair<java.lang.String,Location>	getProofScript()
AbstractProblemLoader.ReplayResult	getReplayResult() Returns the AbstractProblemLoader.ReplayResult if available.
Services	getServices() Returns the Services of getInitConfig().
SpecificationRepository	getSpecificationRepository() Returns the used SpecificationRepository.
U	getUi() Returns the UserInterfaceControl in which the Proof is loaded.
boolean	isDisposed() Checks if this KeYEnvironment is disposed meaning that dispose() was already executed at least once.
static KeYEnvironment<DefaultUserInterfaceControl>	load(java.io.File keyFile)
static KeYEnvironment<DefaultUserInterfaceControl>	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>	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>	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.
static KeYEnvironment<DefaultUserInterfaceControl>	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.

Methods inherited from class java.lang.Object

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

Field Detail

ui

private final U extends UserInterfaceControl ui

The UserInterfaceControl in which the Proof is loaded.

initConfig

private final InitConfig initConfig

The loaded project.

loadedProof

private final Proof loadedProof

An optional Proof which was loaded by the specified proof file.

proofScript

private final Pair<java.lang.String,Location> proofScript

An optional field denoting a script contained in the proof file.

disposed

private boolean disposed

Indicates that this KeYEnvironment is disposed.

replayResult

private final AbstractProblemLoader.ReplayResult replayResult

The AbstractProblemLoader.ReplayResult if available.

Constructor Detail

KeYEnvironment

public KeYEnvironment(U ui,
                      InitConfig initConfig)

Constructor

Parameters:

ui - The UserInterfaceControl in which the Proof is loaded.

initConfig - The loaded project.

KeYEnvironment

public KeYEnvironment(U ui,
                      InitConfig initConfig,
                      Proof loadedProof,
                      Pair<java.lang.String,Location> proofScript,
                      AbstractProblemLoader.ReplayResult replayResult)

Constructor

Parameters:

ui - The UserInterfaceControl in which the Proof is loaded.

initConfig - The loaded project.

Method Detail

getUi

public U getUi()

Returns the UserInterfaceControl in which the Proof is loaded.

Returns:

The UserInterfaceControl in which the Proof is loaded.

getProofControl

public ProofControl getProofControl()

Returns the ProofControl of getUi().

Returns:

The ProofControl of getUi().

getInitConfig

public InitConfig getInitConfig()

Returns the loaded project.

Returns:

The loaded project.

getServices

public Services getServices()

Returns the Services of getInitConfig().

Returns:

The Services of getInitConfig().

getJavaInfo

public JavaInfo getJavaInfo()

Returns the used JavaInfo.

Returns:

The used JavaInfo.

getSpecificationRepository

public SpecificationRepository getSpecificationRepository()

Returns the used SpecificationRepository.

Returns:

The used SpecificationRepository.

getProfile

public Profile getProfile()

getLoadedProof

public Proof getLoadedProof()

Returns the loaded Proof if a proof file was loaded.

Returns:

The loaded Proof if available and null otherwise.

getReplayResult

public AbstractProblemLoader.ReplayResult getReplayResult()

Returns the AbstractProblemLoader.ReplayResult if available.

Returns:

The AbstractProblemLoader.ReplayResult or null if not available.

createProof

public Proof createProof(ProofOblInput input)
                  throws ProofInputException

Creates a new Proof with help of the UserInterfaceControl.

Parameters:

input - The ProofOblInput to instantiate Proof from.

Returns:

The instantiated Proof.

Throws:

ProofInputException - Occurred Exception.

load

public static KeYEnvironment<DefaultUserInterfaceControl> load(java.io.File location,
                                                               java.util.List<java.io.File> classPaths,
                                                               java.io.File bootClassPath,
                                                               java.util.List<java.io.File> includes)
                                                        throws ProblemLoaderException

Loads the given location and returns all required references as KeYEnvironment. The MainWindow is not involved in the whole process.

Parameters:

location - The location to load.

classPaths - The class path entries to use.

bootClassPath - The boot class path to use.

includes - Optional includes to consider.

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

load

public static KeYEnvironment<DefaultUserInterfaceControl> 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)
                                                        throws ProblemLoaderException

Loads the given location and returns all required references as KeYEnvironment. The MainWindow is not involved in the whole process.

Parameters:

location - The location to load.

classPaths - The class path entries to use.

bootClassPath - The boot class path to use.

includes - Optional includes to consider.

ruleCompletionHandler - An optional RuleCompletionHandler.

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

load

public static KeYEnvironment<DefaultUserInterfaceControl> 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)
                                                        throws ProblemLoaderException

Loads the given location and returns all required references as KeYEnvironment. The MainWindow is not involved in the whole process.

Parameters:

profile - The Profile to use.

location - The location to load.

classPaths - The class path entries to use.

bootClassPath - The boot class path to use.

includes - Optional includes to consider.

forceNewProfileOfNewProofs - true #profileOfNewProofs will be used as Profile of new proofs, false Profile specified by problem file will be used for new proofs.

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

load

public static KeYEnvironment<DefaultUserInterfaceControl> 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)
                                                        throws ProblemLoaderException

Loads the given location and returns all required references as KeYEnvironment. The MainWindow is not involved in the whole process.

Parameters:

profile - The Profile to use.

location - The location to load.

classPaths - The class path entries to use.

bootClassPath - The boot class path to use.

includes - Optional includes to consider.

poPropertiesToForce - Some optional PO Properties to force.

ruleCompletionHandler - An optional RuleCompletionHandler.

forceNewProfileOfNewProofs - true AbstractProblemLoader.profileOfNewProofs will be used as Profile of new proofs, false Profile specified by problem file will be used for new proofs.

Returns:

The KeYEnvironment which contains all references to the loaded location.

Throws:

ProblemLoaderException - Occurred Exception

load

public static KeYEnvironment<DefaultUserInterfaceControl> load(java.io.File keyFile)
                                                        throws ProblemLoaderException

Throws:

ProblemLoaderException

dispose

public void dispose()

Disposes this KeYEnvironment.

isDisposed

public boolean isDisposed()

Checks if this KeYEnvironment is disposed meaning that dispose() was already executed at least once.

Returns:

true disposed, false not disposed and still functionable.

getProofScript

public Pair<java.lang.String,Location> getProofScript()