See: Description
| Interface | Description |
|---|---|
| ContractPO |
An obligation for some kind of contract.
|
| DefaultProfileResolver |
Instances of this class are used to get a default
Profile instance. |
| IPersistablePO |
This interface extends the standard proof obligation (
ProofOblInput)
with functionality to define the individual parameters which are required
for loading and saving *.proof files. |
| POExtension |
Instances of this interface are used to customize and extend the behavior of a
ProofOblInput. |
| ProblemInitializer.ProblemInitializerListener | |
| Profile |
This interface provides methods that allow to customize KeY for
certain applications.
|
| ProofOblInput |
Represents something that produces an input proof obligation for the
prover.
|
| Class | Description |
|---|---|
| AbstractOperationPO |
This abstract implementation of
ProofOblInput extends the
functionality of AbstractPO to execute some code within a try catch
block. |
| AbstractPO |
An abstract proof obligation implementing common functionality.
|
| AbstractPO.Vertex |
Represents a vertex and additional information required by the Tarjan algorithm.
|
| AbstractProfile | |
| DependencyContractPO |
The proof obligation for dependency contracts.
|
| FunctionalBlockContractPO |
A proof obligation for a
FunctionalBlockContract. |
| FunctionalLoopContractPO |
A proof obligation for a
FunctionalLoopContract. |
| FunctionalOperationContractPO |
The proof obligation for operation contracts.
|
| Includes |
Encapsulates 2 lists (one for LDT-include, one for "normal" includes)
containing the filenames parsed in the include-section of a
KeYFile. |
| InitConfig |
an instance of this class describes the initial configuration of the prover.
|
| IPersistablePO.LoadedPOContainer |
The class stored in a
Properties instance via key must provide
the static method with the following signature:
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) throws IOException
This method is called by the ProblemLoader to recreate a proof obligation. |
| JavaProfile |
This profile sets up KeY for verification of JavaCard programs.
|
| JavaProfileDefaultProfileResolver |
A
DefaultProfileResolver which returns AbstractProfile.getDefaultProfile(). |
| JavaProfileWithPermissionsDefaultProfileResolver |
A
DefaultProfileResolver which returns JavaProfile.defaultInstancePermissions. |
| KeYUserProblemFile |
Represents an input from a .key user problem file producing an environment
as well as a proof obligation.
|
| ProblemInitializer | |
| ProofInitServiceUtil |
Provides static utility methods to get the following service:
POExtension listed at META-INF/services/de.uka.ilkd.key.proof.init.POExtension
DefaultProfileResolver listed at META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver
|
| ProofObligationVars | |
| RuleCollection |
This class contains the standard rules provided by a profile.
|
| WellDefinednessPO |
The proof obligation for well-definedness checks.
|
| WellDefinednessPO.Variables |
A static data structure for storing and passing the variables used in the actual proof.
|
| Exception | Description |
|---|---|
| ProofInputException |
Reading prover input failed
|