Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Class and Description |
---|---|
class |
AuxiliaryContractConfigurator<T extends AuxiliaryContract>
A window to contain a
AuxiliaryContractSelectionPanel . |
class |
AuxiliaryContractSelectionPanel<T extends AuxiliaryContract>
This panel used to select which
T (s) to use for a
AbstractAuxiliaryContractRule . |
Modifier and Type | Method and Description |
---|---|
void |
AuxiliaryContractSelectionPanel.setContracts(T[] contracts,
java.lang.String title) |
Constructor and Description |
---|
AuxiliaryContractConfigurator(java.lang.String name,
AuxiliaryContractSelectionPanel<T> contractPanel,
java.awt.Frame owner,
Services services,
T[] contracts,
java.lang.String title) |
AuxiliaryContractConfigurator(java.lang.String name,
AuxiliaryContractSelectionPanel<T> contractPanel,
javax.swing.JDialog owner,
Services services,
T[] contracts,
java.lang.String title) |
Modifier and Type | Method and Description |
---|---|
abstract AuxiliaryContract |
AbstractAuxiliaryContractBuiltInRuleApp.getContract() |
Constructor and Description |
---|
ConditionsAndClausesBuilder(AuxiliaryContract contract,
java.util.List<LocationVariable> heaps,
AuxiliaryContract.Variables variables,
Term self,
Services services) |
Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
protected static class |
AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>
This class contains a builder method for
AbstractAuxiliaryContractImpl s
(AbstractAuxiliaryContractImpl.Creator.create() ). |
class |
FunctionalAuxiliaryContract<T extends AuxiliaryContract>
This class is only used to generate a proof obligation for an
AuxiliaryContract . |
Modifier and Type | Interface and Description |
---|---|
interface |
BlockContract
A block contract.
|
interface |
LoopContract
A contract for a block that begins with a loop.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractAuxiliaryContractImpl
Abstract base class for all default implementations of the sub-interfaces of
AuxiliaryContract . |
class |
BlockContractImpl
Default implementation of
BlockContract . |
class |
LoopContractImpl
Default implementation for
LoopContract . |
Modifier and Type | Field and Description |
---|---|
protected T[] |
AbstractAuxiliaryContractImpl.Combinator.contracts
The contracts to combine.
|
Modifier and Type | Method and Description |
---|---|
AuxiliaryContract |
AuxiliaryContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
AuxiliaryContract |
AuxiliaryContract.setBlock(StatementBlock newBlock) |
AuxiliaryContract |
AuxiliaryContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Constructor and Description |
---|
Combinator(T[] contracts,
Services services) |
Modifier and Type | Method and Description |
---|---|
AuxiliaryContract |
IExecutionAuxiliaryContract.getContract()
Returns the applied
AuxiliaryContract . |
Modifier and Type | Method and Description |
---|---|
AuxiliaryContract |
ExecutionAuxiliaryContract.getContract()
Returns the applied
AuxiliaryContract . |
Copyright © 2003-2019 The KeY-Project.