de.uka.ilkd.key.api

Class ProofManagementApi

java.lang.Object

de.uka.ilkd.key.api.ProofManagementApi

public class ProofManagementApi
extends java.lang.Object

This class serves as a facade to all functionalities that are needed for proof management, i.e., loading proof files, retrieving the proof obligations

Author:

Sarah Grebing.

Field Summary

Fields

Modifier and Type	Field and Description
private KeYEnvironment<?>	currentEnv
private java.util.List<Contract>	proofContracts
private java.util.HashSet<java.lang.String>	ruleNames

Constructor Summary

Constructors

Constructor and Description
ProofManagementApi(KeYEnvironment<?> env)

Method Summary

Modifier and Type	Method and Description
private void	buildContracts() constructs the possible proof contracts from the java info in the environment.
ProofApi	getLoadedProof()
java.util.List<Contract>	getProofContracts() Retrieve a list of all available contracts
java.util.Set<java.lang.String>	getRuleNames() Constructs a set containing all names of a taclets that are registered in the current environment.
Services	getServices()
ProofApi	startProof(Contract contract)
ProofApi	startProof(ProofOblInput contract)

Methods inherited from class java.lang.Object

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

Field Detail

currentEnv

private KeYEnvironment<?> currentEnv

proofContracts

private final java.util.List<Contract> proofContracts

ruleNames

private java.util.HashSet<java.lang.String> ruleNames

Constructor Detail

ProofManagementApi

public ProofManagementApi(KeYEnvironment<?> env)

Method Detail

getServices

public Services getServices()

getProofContracts

public java.util.List<Contract> getProofContracts()

Retrieve a list of all available contracts

Returns:

List; can be null if no file was loaded before (we should throw an exception here)

buildContracts

private void buildContracts()

constructs the possible proof contracts from the java info in the environment.

startProof

public ProofApi startProof(ProofOblInput contract)
                    throws ProofInputException

Parameters:

contract -

Returns:

Throws:

ProofInputException

startProof

public ProofApi startProof(Contract contract)
                    throws ProofInputException

Parameters:

contract -

Returns:

Throws:

ProofInputException

getLoadedProof

public ProofApi getLoadedProof()

getRuleNames

public java.util.Set<java.lang.String> getRuleNames()

Constructs a set containing all names of a taclets that are registered in the current environment.

The result is cached to speed up further calls.s

Returns:

always returns a non-null hash set.