Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
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.symbolic_execution.po | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
protected Modality |
LoopInvExecutionPO.getTerminationMarker() |
protected Modality |
InfFlowContractPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
protected Modality |
BlockExecutionPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
protected Modality |
SymbolicExecutionPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.prog(Modality mod,
JavaBlock jb,
Term t) |
Term |
TermBuilder.prog(Modality mod,
JavaBlock jb,
Term t,
ImmutableArray<TermLabel> labels) |
Modifier and Type | Field and Description |
---|---|
static Modality |
Modality.BOX
The box operator of dynamic logic.
|
static Modality |
Modality.BOX_TRANSACTION
A Java Card transaction version of the box modality.
|
static Modality |
Modality.DIA
The diamond operator of dynamic logic.
|
static Modality |
Modality.DIA_TRANSACTION
A Java Card transaction version of the diamond modality.
|
static Modality |
Modality.TOUT
The throughout operator of dynamic logic.
|
static Modality |
Modality.TOUT_TRANSACTION
A Java Card transaction version of the throughout modality.
|
Modifier and Type | Method and Description |
---|---|
static Modality |
Modality.getModality(java.lang.String str)
Returns a modality corresponding to a string
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Modality> |
ModalOperatorSV.getModalities()
returns an unmodifiable set of operators this schemavariable can match
|
Modifier and Type | Method and Description |
---|---|
static ModalOperatorSV |
SchemaVariableFactory.createModalOperatorSV(Name name,
Sort sort,
ImmutableSet<Modality> modalities)
creates a SchemaVariable representing an operator
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<Modality> |
ExpressionBuilder.opSVHelper(java.lang.String opName,
ImmutableSet<Modality> modalities) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<Modality> |
ExpressionBuilder.opSVHelper(java.lang.String opName,
ImmutableSet<Modality> modalities) |
Modifier and Type | Method and Description |
---|---|
protected abstract Modality |
AbstractOperationPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
protected Modality |
FunctionalOperationContractPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<BlockContract> |
SpecificationRepository.getBlockContracts(StatementBlock block,
Modality modality)
Returns block contracts for according block statement
and modality.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(LoopStatement loop,
Modality modality)
Returns loop contracts for according loop statement
and modality.
|
ImmutableSet<LoopContract> |
SpecificationRepository.getLoopContracts(StatementBlock block,
Modality modality) |
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm,
Modality modality)
Returns all registered (atomic) operation contracts for the passed
operation which refer to the passed modality.
|
Modifier and Type | Field and Description |
---|---|
Modality |
UseOperationContractRule.Instantiation.mod
The modality.
|
Modality |
AbstractAuxiliaryContractRule.Instantiation.modality
The contract's modality.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<BlockContract> |
AbstractBlockContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
static ImmutableSet<LoopContract> |
AbstractLoopContractRule.getApplicableContracts(SpecificationRepository specifications,
JavaStatement statement,
Modality modality,
Goal goal) |
protected boolean |
AbstractBlockContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
protected abstract boolean |
AbstractAuxiliaryContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement element,
Modality modality,
Goal goal) |
protected boolean |
AbstractLoopContractRule.Instantiator.hasApplicableContracts(Services services,
JavaStatement statement,
Modality modality,
Goal goal) |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
Instantiation(Term update,
Term formula,
Modality modality,
Term self,
JavaStatement statement,
ExecutionContext context) |
Modifier and Type | Field and Description |
---|---|
protected Modality |
AbstractAuxiliaryContractImpl.modality |
Modifier and Type | Method and Description |
---|---|
Modality |
AbstractAuxiliaryContractImpl.getModality() |
Modality |
FunctionalAuxiliaryContract.getModality() |
Modality |
FunctionalOperationContractImpl.getModality() |
Modality |
InformationFlowContractImpl.getModality() |
Modality |
InformationFlowContract.getModality()
Returns the modality of the contract.
|
Modality |
FunctionalOperationContract.getModality()
Returns the modality of the contract.
|
Modality |
AuxiliaryContract.getModality() |
Modifier and Type | Method and Description |
---|---|
protected abstract T |
AbstractAuxiliaryContractImpl.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.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.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) |
InformationFlowContract |
ContractFactory.createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariableCollection progVars,
boolean toBeSaved,
boolean transaction)
Creates a new functional operation contract.
|
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
KeYJavaType kjt,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accs,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
boolean toBeSaved)
Creates a new functional operation contract.
|
InformationFlowContract |
InformationFlowContractImpl.setModality(Modality modality) |
InformationFlowContract |
InformationFlowContract.setModality(Modality modality) |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(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,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
BlockContractImpl(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,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
InformationFlowContractImpl(java.lang.String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
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,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(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,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
Modifier and Type | Method and Description |
---|---|
protected Modality |
ProgramMethodPO.getTerminationMarker()
Returns the
Modality to use as termination marker. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<LocationVariable> |
MiscTools.applicableHeapContexts(Modality modality,
Services services)
Returns the applicable heap contexts out of the currently available set
of three contexts: The normal heap, the saved heap (transaction), and the
permission heap.
|
static boolean |
MiscTools.isTransaction(Modality modality)
Checks whether the given
Modality is a transaction modality. |
Copyright © 2003-2019 The KeY-Project.