Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
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 |
Modifier and Type | Method and Description |
---|---|
LoopContract |
LoopContractSelectionPanel.computeContract(Services services,
java.util.List<LoopContract> selection) |
Modifier and Type | Method and Description |
---|---|
LoopContract |
LoopContractSelectionPanel.computeContract(Services services,
java.util.List<LoopContract> selection) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnLoopContract(LoopContract x) |
void |
JavaASTVisitor.performActionOnLoopContract(LoopContract x) |
void |
ProgramVariableCollector.performActionOnLoopContract(LoopContract x) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop)
Returns all loop contracts for the specified loop.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop,
Modality modality)
Returns loop contracts for according loop statement
and modality.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block)
Returns all loop contracts for the specified block.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block,
Modality modality) |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addLoopContract(LoopContract contract)
Adds a new
LoopContract and a new FunctionalLoopContract
to the repository. |
void |
SpecificationRepository.addLoopContract(LoopContract contract,
boolean addFunctionalContract)
Adds a new
LoopContract to the repository. |
void |
SpecificationRepository.removeLoopContract(LoopContract contract)
Removes a
LoopContract from the repository. |
Modifier and Type | Field and Description |
---|---|
protected LoopContract |
AbstractLoopContractBuiltInRuleApp.contract |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<LoopContract> |
LoopApplyHeadBuiltInRuleApp.contracts
The loop contracts on which the rule is applied.
|
Modifier and Type | Method and Description |
---|---|
LoopContract |
AbstractLoopContractBuiltInRuleApp.getContract() |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<LoopContract> |
AbstractLoopContractRule.filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
Goal goal) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
Goal goal,
Services services) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected static boolean |
AbstractLoopContractRule.contractApplied(LoopContract contract,
Goal goal) |
protected java.util.Map<LocationVariable,Function> |
AbstractLoopContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
LoopContract contract,
TermServices services) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
void |
AbstractLoopContractBuiltInRuleApp.update(JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<LoopContract> |
AbstractLoopContractRule.filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
Goal goal) |
Constructor and Description |
---|
LoopContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
LoopContractInternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
LoopContract contract,
java.util.List<LocationVariable> heaps) |
Constructor and Description |
---|
LoopApplyHeadBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableSet<LoopContract> contracts) |
Modifier and Type | Class and Description |
---|---|
class |
LoopContractImpl
Default implementation for
LoopContract . |
Modifier and Type | Method and Description |
---|---|
protected LoopContract |
LoopContractImpl.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 LoopContract |
LoopContractImpl.Combinator.combine() |
static LoopContract |
LoopContractImpl.combine(ImmutableSet<LoopContract> contracts,
Services services) |
LoopContract |
LoopContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopContract |
LoopContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
LoopContract |
LoopContract.replaceEnhancedForVariables(StatementBlock newBlock,
Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
LoopContract |
LoopContractImpl.replaceEnhancedForVariables(StatementBlock newBlock,
Services services) |
LoopContract |
LoopContract.setBlock(StatementBlock newBlock) |
LoopContract |
LoopContractImpl.setBlock(StatementBlock newBlock) |
LoopContract |
LoopContract.setLoop(LoopStatement newLoop) |
LoopContract |
LoopContractImpl.setLoop(LoopStatement newLoop) |
LoopContract |
LoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
LoopContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
BlockContractImpl.toLoopContract() |
LoopContract |
BlockContract.toLoopContract() |
LoopContract |
LoopContract.update(LoopStatement newLoop,
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,
Term newDecreases) |
LoopContract |
LoopContractImpl.update(LoopStatement newLoop,
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,
Term newDecreases) |
LoopContract |
LoopContract.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,
Term newDecreases) |
LoopContract |
LoopContractImpl.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,
Term newDecreases) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled)
Returns the loop contracts for the passed labeled statement if it labels
a block.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop)
Returns the loop contracts for the passed loop.
|
ImmutableSet<LoopContract> |
SpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block)
Returns the loop contracts for the passed block.
|
Modifier and Type | Method and Description |
---|---|
FunctionalLoopContract |
ContractFactory.funcLoop(LoopContract loopContract)
Create a new
FunctionalLoopContract from an existing LoopContract . |
Modifier and Type | Method and Description |
---|---|
static LoopContract |
LoopContractImpl.combine(ImmutableSet<LoopContract> contracts,
Services services) |
Constructor and Description |
---|
Combinator(LoopContract[] contracts,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LabeledStatement labeled) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
LoopStatement loop) |
ImmutableSet<LoopContract> |
JMLSpecExtractor.extractLoopContracts(IProgramMethod method,
StatementBlock block) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
LoopStatement loop,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a loop from a textual specification case.
|
ImmutableSet<LoopContract> |
JMLSpecFactory.createJMLLoopContracts(IProgramMethod method,
java.util.List<Label> labels,
StatementBlock block,
TextualJMLSpecCase specificationCase)
Creates a set of loop contracts for a block from a textual specification case.
|
Copyright © 2003-2019 The KeY-Project.