Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
ProofApi |
ProofManagementApi.startProof(ProofOblInput contract) |
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractUserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
Proof |
UserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
Proof |
KeYEnvironment.createProof(ProofOblInput input)
Creates a new
Proof with help of the UserInterfaceControl . |
protected abstract ProofEnvironment |
AbstractUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
ProofEnvironment |
DefaultUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
void |
DefaultUserInterfaceControl.reportException(java.lang.Object sender,
ProofOblInput input,
java.lang.Exception e) |
Modifier and Type | Method and Description |
---|---|
void |
WindowUserInterfaceControl.reportException(java.lang.Object sender,
ProofOblInput input,
java.lang.Exception e) |
Modifier and Type | Interface and Description |
---|---|
interface |
InfFlowCompositePO |
interface |
InfFlowLeafPO |
interface |
InfFlowPO |
Modifier and Type | Class and Description |
---|---|
class |
AbstractInfFlowPO
Abstract to customize
AbstractPO and AbstractOperationPO . |
class |
BlockExecutionPO |
class |
InfFlowContractPO |
class |
LoopInvExecutionPO |
class |
SymbolicExecutionPO |
Modifier and Type | Method and Description |
---|---|
boolean |
LoopInvExecutionPO.implies(ProofOblInput po) |
boolean |
InfFlowContractPO.implies(ProofOblInput po) |
boolean |
BlockExecutionPO.implies(ProofOblInput po) |
boolean |
SymbolicExecutionPO.implies(ProofOblInput po) |
Modifier and Type | Interface and Description |
---|---|
interface |
ContractPO
An obligation for some kind of contract.
|
interface |
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. |
Modifier and Type | Class and Description |
---|---|
class |
AbstractOperationPO
This abstract implementation of
ProofOblInput extends the
functionality of AbstractPO to execute some code within a try catch
block. |
class |
AbstractPO
An abstract proof obligation implementing common functionality.
|
class |
DependencyContractPO
The proof obligation for dependency contracts.
|
class |
FunctionalBlockContractPO
A proof obligation for a
FunctionalBlockContract . |
class |
FunctionalLoopContractPO
A proof obligation for a
FunctionalLoopContract . |
class |
FunctionalOperationContractPO
The proof obligation for operation contracts.
|
class |
KeYUserProblemFile
Represents an input from a .key user problem file producing an environment
as well as a proof obligation.
|
class |
WellDefinednessPO
The proof obligation for well-definedness checks.
|
Modifier and Type | Method and Description |
---|---|
ProofOblInput |
IPersistablePO.LoadedPOContainer.getProofOblInput()
Returns the created
ProofOblInput . |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<POExtension> |
ProofInitServiceUtil.getOperationPOExtension(ProofOblInput po)
Returns the
POExtension which supports the given ProofOblInput . |
boolean |
DependencyContractPO.implies(ProofOblInput po) |
boolean |
FunctionalBlockContractPO.implies(ProofOblInput po) |
boolean |
KeYUserProblemFile.implies(ProofOblInput po) |
boolean |
WellDefinednessPO.implies(ProofOblInput po) |
boolean |
ProofOblInput.implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
boolean |
FunctionalLoopContractPO.implies(ProofOblInput po) |
boolean |
FunctionalOperationContractPO.implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
boolean |
AbstractPO.implies(ProofOblInput po) |
boolean |
POExtension.isPOSupported(ProofOblInput po)
Checks if the given
ProofOblInput is supported. |
void |
ProblemInitializer.ProblemInitializerListener.reportException(java.lang.Object sender,
ProofOblInput input,
java.lang.Exception e) |
ProofAggregate |
ProblemInitializer.startProver(EnvInput envInput,
ProofOblInput po) |
ProofAggregate |
ProblemInitializer.startProver(InitConfig initConfig,
ProofOblInput po) |
Constructor and Description |
---|
LoadedPOContainer(ProofOblInput proofOblInput)
Constructor.
|
LoadedPOContainer(ProofOblInput proofOblInput,
int proofNum)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
ProofOblInput |
ProofEnvironmentEvent.getPo() |
ProofOblInput |
SpecificationRepository.getProofOblInput(Proof proof)
Returns the
ProofOblInput from which the given Proof was
created. |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(ProofOblInput po)
Returns all proofs registered for the passed PO (or stronger POs).
|
void |
SpecificationRepository.registerProof(ProofOblInput po,
Proof proof)
Registers the passed proof.
|
void |
ProofEnvironment.registerProof(ProofOblInput po,
ProofAggregate pl)
registers a proof loaded with the given
ProofOblInput . |
Constructor and Description |
---|
ProofEnvironmentEvent(ProofEnvironment source,
ProofOblInput po,
ProofAggregate proofList) |
Modifier and Type | Method and Description |
---|---|
ProofOblInput |
FunctionalAuxiliaryContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
InformationFlowContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalBlockContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
DependencyContractImpl.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
WellDefinednessCheck.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
Contract.createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
FunctionalLoopContract.createProofObl(InitConfig initConfig,
Contract contract) |
ProofOblInput |
FunctionalAuxiliaryContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
ProofOblInput |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
InformationFlowContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
FunctionalBlockContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
ProofOblInput |
DependencyContractImpl.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
WellDefinednessCheck.createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel) |
ProofOblInput |
Contract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
FunctionalLoopContract.createProofObl(InitConfig initConfig,
Contract contract,
boolean supportSymbolicExecutionAPI) |
ProofOblInput |
FunctionalAuxiliaryContract.getProofObl(Services services) |
ProofOblInput |
FunctionalOperationContractImpl.getProofObl(Services services) |
ProofOblInput |
InformationFlowContractImpl.getProofObl(Services services) |
ProofOblInput |
DependencyContractImpl.getProofObl(Services services) |
ProofOblInput |
WellDefinednessCheck.getProofObl(Services services) |
ProofOblInput |
Contract.getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramMethodPO
This proof obligation executes an
IProgramMethod with
an optional precondition. |
class |
ProgramMethodSubsetPO
This proof obligation executes selected statements of the body
of a given
IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
boolean |
TruthValuePOExtension.isPOSupported(ProofOblInput po)
Checks if the given
ProofOblInput is supported. |
Modifier and Type | Class and Description |
---|---|
class |
TacletProofObligationInput
The Class TacletProofObligationInput is a special purpose proof obligations
for taclet proofs.
|
Modifier and Type | Method and Description |
---|---|
abstract ProofOblInput |
TacletLoader.getTacletFile(Proof proof)
subclasses give a special proof obligation input per proof.
|
ProofOblInput |
TacletLoader.TacletFromFileLoader.getTacletFile(Proof proof) |
ProofOblInput |
TacletLoader.KeYsTacletsLoader.getTacletFile(Proof proof) |
Modifier and Type | Method and Description |
---|---|
boolean |
TacletProofObligationInput.implies(ProofOblInput po) |
Modifier and Type | Method and Description |
---|---|
protected ProofOblInput |
ConsoleProofObligationSelector.createPOForSelectedContract() |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
AbstractMediatorUserInterfaceControl.createProofEnvironmentAndRegisterProof(ProofOblInput proofOblInput,
ProofAggregate proofList,
InitConfig initConfig)
registers the proof aggregate at the UI
|
protected void |
ConsoleProofObligationSelector.findOrStartProof(ProofOblInput po) |
void |
ConsoleUserInterfaceControl.reportException(java.lang.Object sender,
ProofOblInput input,
java.lang.Exception e) |
Modifier and Type | Class and Description |
---|---|
static class |
ProofStarter.UserProvidedInput
Proof obligation for a given formula or sequent
|
Modifier and Type | Method and Description |
---|---|
boolean |
ProofStarter.UserProvidedInput.implies(ProofOblInput po) |
Copyright © 2003-2019 The KeY-Project.