Package | Description |
---|---|
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.informationflow.po.snippet | |
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
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 | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractSelectionPanel.computeBlockContract(Services services,
java.util.List<BlockContract> selection)
The static access is used e.g.
|
BlockContract |
BlockContractSelectionPanel.computeContract(Services services,
java.util.List<BlockContract> selection)
Computes the selected
BlockContract . |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractSelectionPanel.computeBlockContract(Services services,
java.util.List<BlockContract> selection)
The static access is used e.g.
|
BlockContract |
BlockContractSelectionPanel.computeContract(Services services,
java.util.List<BlockContract> selection)
Computes the selected
BlockContract . |
Constructor and Description |
---|
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(BlockContract contract,
ProofObligationVars vars,
ExecutionContext context,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(BlockContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
InfFlowBlockContractTacletBuilder.setContract(BlockContract contract) |
void |
BlockInfFlowUnfoldTacletBuilder.setContract(BlockContract c) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnBlockContract(BlockContract x) |
void |
JavaASTVisitor.performActionOnBlockContract(BlockContract x) |
void |
ProgramVariableCollector.performActionOnBlockContract(BlockContract x) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block)
Returns all block contracts for the specified block.
|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block,
Modality modality)
Returns block contracts for according block statement
and modality.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addBlockContract(BlockContract contract)
Adds a new
BlockContract and a new FunctionalBlockContract
to the repository. |
void |
SpecificationRepository.addBlockContract(BlockContract contract,
boolean addFunctionalContract)
Adds a new
BlockContract to the repository. |
void |
SpecificationRepository.removeBlockContract(BlockContract contract)
Removes a
BlockContract from the repository. |
Modifier and Type | Field and Description |
---|---|
protected BlockContract |
AbstractBlockContractBuiltInRuleApp.contract |
Modifier and Type | Method and Description |
---|---|
BlockContract |
AbstractBlockContractBuiltInRuleApp.getContract() |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<BlockContract> |
AbstractBlockContractRule.filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected static boolean |
AbstractBlockContractRule.contractApplied(BlockContract contract,
Goal goal) |
protected static java.util.Map<LocationVariable,Function> |
AbstractBlockContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
void |
AbstractBlockContractBuiltInRuleApp.update(JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<BlockContract> |
AbstractBlockContractRule.filterAppliedContracts(ImmutableSet<BlockContract> collectedContracts,
Goal goal) |
Constructor and Description |
---|
BlockContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
BlockContractInternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Class and Description |
---|---|
class |
BlockContractImpl
Default implementation of
BlockContract . |
Modifier and Type | Method and Description |
---|---|
protected BlockContract |
BlockContractImpl.Creator.build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
protected BlockContract |
BlockContractImpl.Combinator.combine() |
static BlockContract |
BlockContractImpl.combine(ImmutableSet<BlockContract> contracts,
Services services) |
BlockContract |
BlockWellDefinedness.getStatement() |
BlockContract |
BlockContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
BlockContract |
BlockContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
BlockContract |
BlockContractImpl.setBlock(StatementBlock newBlock) |
BlockContract |
BlockContract.setBlock(StatementBlock newBlock) |
BlockContract |
BlockContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
BlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
LoopContract.toBlockContract()
Returns a
BlockContract for AuxiliaryContract.getBlock() . |
BlockContract |
LoopContractImpl.toBlockContract() |
BlockContract |
BlockContractImpl.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newinfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
BlockContract |
BlockContract.update(StatementBlock newBlock,
java.util.Map<LocationVariable,Term> newPreconditions,
java.util.Map<LocationVariable,Term> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the block contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<BlockContract> |
SpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block)
Returns the block contracts for the passed block.
|
Modifier and Type | Method and Description |
---|---|
FunctionalBlockContract |
ContractFactory.funcBlock(BlockContract blockContract)
Create a new
FunctionalBlockContract from an existing BlockContract . |
Modifier and Type | Method and Description |
---|---|
static BlockContract |
BlockContractImpl.combine(ImmutableSet<BlockContract> contracts,
Services services) |
Constructor and Description |
---|
BlockWellDefinedness(BlockContract block,
AuxiliaryContract.Variables variables,
ImmutableSet<ProgramVariable> params,
Services services)
Creates a contract to check well-definedness of a block contract
|
Combinator(BlockContract[] contracts,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<BlockContract> |
JMLSpecExtractor.extractBlockContracts(IProgramMethod method,
StatementBlock block) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
JMLSpecFactory.createJMLBlockContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of block contracts for a block from a textual specification case.
|
Modifier and Type | Method and Description |
---|---|
BlockContract |
ExecutionNodeReader.KeYlessBlockContract.getContract()
Returns the applied
AuxiliaryContract . |
Copyright © 2003-2019 The KeY-Project.