Class and Description |
---|
ProofInputException
Reading prover input failed
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
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. |
ProblemInitializer |
ProblemInitializer.ProblemInitializerListener |
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
Class and Description |
---|
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. |
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 and Description |
---|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
Class and 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.
|
ContractPO
An obligation for some kind of contract.
|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
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. |
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. |
ProofInputException
Reading prover input failed
|
ProofObligationVars |
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
ProofObligationVars |
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
Class and Description |
---|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
Class and Description |
---|
Includes
Encapsulates 2 lists (one for LDT-include, one for "normal" includes)
containing the filenames parsed in the include-section of a
KeYFile . |
Class and Description |
---|
Includes
Encapsulates 2 lists (one for LDT-include, one for "normal" includes)
containing the filenames parsed in the include-section of a
KeYFile . |
Class and Description |
---|
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.
|
Class and 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.
|
AbstractProfile |
ContractPO
An obligation for some kind of contract.
|
DefaultProfileResolver
Instances of this class are used to get a default
Profile instance. |
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
This interface extends the standard proof obligation (
ProofOblInput )
with functionality to define the individual parameters which are required
for loading and saving *.proof files. |
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.
|
KeYUserProblemFile
Represents an input from a .key user problem file producing an environment
as well as a proof obligation.
|
POExtension
Instances of this interface are used to customize and extend the behavior of a
ProofOblInput . |
ProblemInitializer |
ProblemInitializer.ProblemInitializerListener |
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
ProofObligationVars |
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
RuleCollection
This class contains the standard rules provided by a profile.
|
Class and Description |
---|
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. |
ProblemInitializer |
ProblemInitializer.ProblemInitializerListener |
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
ContractPO
An obligation for some kind of contract.
|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
ProofObligationVars |
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
ContractPO
An obligation for some kind of contract.
|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
WellDefinednessPO.Variables
A static data structure for storing and passing the variables used in the actual proof.
|
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProofInputException
Reading prover input failed
|
Class and 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.
|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
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. |
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. |
POExtension
Instances of this interface are used to customize and extend the behavior of a
ProofOblInput . |
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
AbstractProfile |
DefaultProfileResolver
Instances of this class are used to get a default
Profile instance. |
InitConfig
an instance of this class describes the initial configuration of the prover.
|
JavaProfile
This profile sets up KeY for verification of JavaCard programs.
|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProofInputException
Reading prover input failed
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
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. |
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. |
ProblemInitializer |
ProblemInitializer.ProblemInitializerListener |
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Class and Description |
---|
InitConfig
an instance of this class describes the initial configuration of the prover.
|
ProblemInitializer |
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 and Description |
---|
Profile
This interface provides methods that allow to customize KeY for
certain applications.
|
ProofInputException
Reading prover input failed
|
ProofOblInput
Represents something that produces an input proof obligation for the
prover.
|
Copyright © 2003-2019 The KeY-Project.