Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.symbolic_execution.po |
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 | 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 |
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 |
WellDefinednessPO
The proof obligation for well-definedness checks.
|
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 . |
Copyright © 2003-2019 The KeY-Project.