Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.nparser.builder | |
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.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.speclang.jml.translation | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.testgen | |
de.uka.ilkd.key.ui |
Modifier and Type | Method and Description |
---|---|
java.util.List<Contract> |
ProofManagementApi.getProofContracts()
Retrieve a list of all available contracts
|
Modifier and Type | Method and Description |
---|---|
ProofApi |
ProofManagementApi.startProof(Contract contract) |
Modifier and Type | Method and Description |
---|---|
static Contract |
ContractSelectionPanel.computeContract(Services services,
java.util.List<Contract> selection)
Computes the selected
Contract . |
Contract |
ContractConfigurator.getContract()
Returns the selected contract.
|
Contract |
ContractSelectionPanel.getContract() |
Modifier and Type | Method and Description |
---|---|
void |
ContractSelectionPanel.selectContract(Contract contract)
Selects the given contract in the list.
|
void |
ContractSelectionPanel.setContracts(Contract[] contracts,
java.lang.String title) |
Modifier and Type | Method and Description |
---|---|
static Contract |
ContractSelectionPanel.computeContract(Services services,
java.util.List<Contract> selection)
Computes the selected
Contract . |
void |
ContractSelectionPanel.setContracts(ImmutableSet<Contract> contracts,
java.lang.String title) |
Constructor and Description |
---|
ContractConfigurator(java.awt.Frame owner,
Services services,
Contract[] contracts,
java.lang.String title,
boolean allowMultipleContracts) |
ContractConfigurator(javax.swing.JDialog owner,
Services services,
Contract[] contracts,
java.lang.String title,
boolean allowMultipleContracts) |
Modifier and Type | Method and Description |
---|---|
java.util.List<Contract> |
ContractsAndInvariantsFinder.getContracts() |
Modifier and Type | Method and Description |
---|---|
Contract |
FunctionalBlockContractPO.getContract() |
Contract |
ContractPO.getContract() |
Contract |
FunctionalLoopContractPO.getContract() |
Modifier and Type | Method and Description |
---|---|
Contract |
SpecificationRepository.getContractByName(java.lang.String name)
Returns the registered (atomic or combined) contract corresponding to the
passed name, or null.
|
Contract |
RuleJustificationBySpec.getSpec() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Contract> |
SpecificationRepository.getAllContracts()
Returns all registered contracts.
|
ImmutableSet<Contract> |
SpecificationRepository.getContracts(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) contracts for the passed target.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(Contract contract)
Returns a set encompassing the passed contract and all its versions
inherited to overriding methods.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(ImmutableSet<Contract> contractSet)
Returns a set encompassing the passed contracts and all its versions
inherited to overriding methods.
|
ImmutableSet<Contract> |
ProofCorrectnessMgt.getUsedContracts() |
ImmutableSet<Contract> |
SpecificationRepository.splitContract(Contract contract)
Splits the passed contract into its atomic components.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addContract(Contract contract)
Registers the passed (atomic) contract, and inherits it to all overriding
methods.
|
void |
SpecificationRepository.addContractNoInheritance(Contract contract)
Registers the passed (atomic) contract without inheriting it.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(Contract contract)
Returns a set encompassing the passed contract and all its versions
inherited to overriding methods.
|
ContractPO |
SpecificationRepository.getPO(Contract c)
Returns the PO that the passed contract is about, or null.
|
ImmutableSet<Proof> |
SpecificationRepository.getProofs(Contract atomicContract)
Returns all proofs registered for the passed atomic contract, or for
combined contracts including the passed atomic contract
|
boolean |
ProofCorrectnessMgt.isContractApplicable(Contract contract)
Tells whether a contract for the passed target may be applied
in the passed goal without creating circular dependencies.
|
ImmutableSet<Contract> |
SpecificationRepository.splitContract(Contract contract)
Splits the passed contract into its atomic components.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addContracts(ImmutableSet<Contract> toAdd)
Registers the passed contracts.
|
ImmutableSet<Contract> |
SpecificationRepository.getInheritedContracts(ImmutableSet<Contract> contractSet)
Returns a set encompassing the passed contracts and all its versions
inherited to overriding methods.
|
Constructor and Description |
---|
RuleJustificationBySpec(Contract spec) |
Modifier and Type | Field and Description |
---|---|
protected Contract |
AbstractContractRuleApp.instantiation |
Modifier and Type | Method and Description |
---|---|
Contract |
AbstractContractRuleApp.getInstantiation() |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Contract> |
UseDependencyContractRule.getApplicableContracts(Services services,
KeYJavaType kjt,
IObserverFunction target)
Returns the dependency contracts which are applicable for the passed
target.
|
Modifier and Type | Method and Description |
---|---|
UseDependencyContractApp |
UseDependencyContractApp.setContract(Contract contract) |
abstract AbstractContractRuleApp |
AbstractContractRuleApp.setContract(Contract contract) |
ContractRuleApp |
ContractRuleApp.setContract(Contract contract) |
Constructor and Description |
---|
AbstractContractRuleApp(BuiltInRule rule,
PosInOccurrence pio,
Contract contract) |
AbstractContractRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Contract contract) |
UseDependencyContractApp(BuiltInRule builtInRule,
PosInOccurrence pio,
Contract instantiation,
PosInOccurrence step) |
UseDependencyContractApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Contract contract,
PosInOccurrence step) |
Modifier and Type | Interface and Description |
---|---|
interface |
DependencyContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
interface |
FunctionalOperationContract
A contract about an operation (i.e., a method or a constructor), consisting
of a precondition, a postcondition, a modifies clause, a measured-by clause,
and a modality.
|
interface |
InformationFlowContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
interface |
OperationContract |
Modifier and Type | Class and Description |
---|---|
class |
BlockWellDefinedness
A contract for checking the well-definedness of a jml block contract.
|
class |
ClassWellDefinedness
A contract for checking the well-definedness of a specification for a class invariant.
|
class |
DependencyContractImpl
Standard implementation of the DependencyContract interface.
|
class |
FunctionalAuxiliaryContract<T extends AuxiliaryContract>
This class is only used to generate a proof obligation for an
AuxiliaryContract . |
class |
FunctionalBlockContract
This class is only used to generate a proof obligation for a block (see
FunctionalBlockContractPO . |
class |
FunctionalLoopContract
This class is only used to generate a proof obligation for a block that starts with a loop (see
FunctionalLoopContractPO . |
class |
FunctionalOperationContractImpl
Standard implementation of the OperationContract interface.
|
class |
InformationFlowContractImpl
Standard implementation of the DependencyContract interface.
|
class |
LoopWellDefinedness
A contract for checking the well-definedness of a jml loop invariant.
|
class |
MethodWellDefinedness
A contract for checking the well-definedness of a specification for a method or model field.
|
class |
StatementWellDefinedness
A contract for checking the well-definedness of a jml statement.
|
class |
WellDefinednessCheck
A contract for checking the well-definedness of a jml specification element
(i.e.
|
Modifier and Type | Method and Description |
---|---|
Contract |
MethodWellDefinedness.getMethodContract() |
Contract |
Contract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
Contract |
FunctionalBlockContract.setID(int newId) |
Contract |
Contract.setID(int newId)
Returns a contract which is identical this contract except that the id is set to the new id.
|
Contract |
LoopWellDefinedness.setID(int newId) |
Contract |
BlockWellDefinedness.setID(int newId) |
Contract |
FunctionalLoopContract.setID(int newId) |
Contract |
FunctionalOperationContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalBlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
DependencyContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
Contract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Returns a contract which is identical to this contract except that the KeYJavaType and
IObserverFunction are set to the new values.
|
Contract |
LoopWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
BlockWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalLoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
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) |
boolean |
InformationFlowContractImpl.equals(Contract c) |
boolean |
InformationFlowContract.equals(Contract c) |
Modifier and Type | Method and Description |
---|---|
Contract |
JMLSpecFactory.createJMLDependencyContract(KeYJavaType kjt,
LocationVariable targetHeap,
LabeledParserRuleContext originalDep) |
Contract |
JMLSpecFactory.createJMLDependencyContract(KeYJavaType kjt,
TextualJMLDepends textualDep) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Contract> |
JMLSpecFactory.createFunctionalOperationContracts(java.lang.String name,
IProgramMethod pm,
ProgramVariableCollection progVars,
JMLSpecFactory.ContractClauses clauses,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> axioms)
Generate functional operation contracts.
|
ImmutableSet<Contract> |
JMLSpecFactory.createJMLOperationContracts(IProgramMethod pm,
TextualJMLSpecCase textualSpecCase)
Creates operation contracts out of the passed JML specification.
|
Modifier and Type | Method and Description |
---|---|
Contract |
ExecutionNodeReader.KeYlessOperationContract.getContract()
Returns the applied
Contract . |
Modifier and Type | Method and Description |
---|---|
Contract |
IExecutionOperationContract.getContract()
Returns the applied
Contract . |
Modifier and Type | Method and Description |
---|---|
Contract |
ExecutionOperationContract.getContract()
Returns the applied
Contract . |
Modifier and Type | Method and Description |
---|---|
Contract |
ProofInfo.getContract() |
Modifier and Type | Field and Description |
---|---|
protected java.util.List<Contract> |
ConsoleProofObligationSelector.contracts |
Copyright © 2003-2019 The KeY-Project.