Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po.snippet | |
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
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.dl.translation | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Method and Description |
---|---|
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(FunctionalOperationContract contract,
ProofObligationVars vars,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
InfFlowMethodContractTacletBuilder.setContract(FunctionalOperationContract contract) |
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
FunctionalOperationContractPO.getContract() |
Constructor and Description |
---|
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract)
Constructor.
|
FunctionalOperationContractPO(InitConfig initConfig,
FunctionalOperationContract contract,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
SpecificationRepository.combineOperationContracts(ImmutableSet<FunctionalOperationContract> toCombine)
Creates a combined contract out of the passed atomic contracts.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm)
Returns all registered (atomic) operation contracts for the passed
operation.
|
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 | Method and Description |
---|---|
FunctionalOperationContract |
SpecificationRepository.combineOperationContracts(ImmutableSet<FunctionalOperationContract> toCombine)
Creates a combined contract out of the passed atomic contracts.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<FunctionalOperationContract> |
UseOperationContractRule.getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services)
Returns the operation contracts which are applicable for the passed instantiation.
|
Modifier and Type | Class and Description |
---|---|
class |
FunctionalOperationContractImpl
Standard implementation of the OperationContract interface.
|
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
ContractFactory.addGlobalDefs(FunctionalOperationContract opc,
Term globalDefs)
Add global variable definitions (aka.
|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
InitiallyClause ini)
Add the specification contained in InitiallyClause as a postcondition.
|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
Term addedPost,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
postcondition (regardless of termination case).
|
FunctionalOperationContract |
ContractFactory.addPre(FunctionalOperationContract old,
Term addedPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
precondition.
|
FunctionalOperationContract |
ContractFactory.func(IProgramMethod pm,
InitiallyClause ini)
|
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
IProgramMethod pm,
boolean terminates,
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 pv)
Creates a new functional operation contract.
|
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.
|
FunctionalOperationContract |
FunctionalOperationContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
FunctionalOperationContract |
FunctionalOperationContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
FunctionalOperationContract |
FunctionalOperationContractImpl.setID(int newId) |
FunctionalOperationContract |
ContractFactory.union(FunctionalOperationContract... contracts)
Returns the union of the passed contracts.
|
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
ContractFactory.addGlobalDefs(FunctionalOperationContract opc,
Term globalDefs)
Add global variable definitions (aka.
|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
InitiallyClause ini)
Add the specification contained in InitiallyClause as a postcondition.
|
FunctionalOperationContract |
ContractFactory.addPost(FunctionalOperationContract old,
Term addedPost,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
postcondition (regardless of termination case).
|
FunctionalOperationContract |
ContractFactory.addPre(FunctionalOperationContract old,
Term addedPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
precondition.
|
static java.lang.String |
FunctionalOperationContractImpl.getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
FunctionalOperationContract |
ContractFactory.union(FunctionalOperationContract... contracts)
Returns the union of the passed contracts.
|
Constructor and Description |
---|
MethodWellDefinedness(FunctionalOperationContract contract,
Services services) |
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
DLSpecFactory.createDLOperationContract(java.lang.String name,
Term fma,
Term modifies)
Creates an operation contract from an implication formula of the form
"pre -> {heapAtPre := heap}
[#catchAll(java.lang.Throwable exc){m();}]post",
(where the update and/or the #catchAll may be omitted) and a modifies
clause.
|
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
JMLSpecFactory.initiallyClauseToContract(InitiallyClause ini,
IProgramMethod pm)
Translate initially clause to a contract for the given constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionOperationContract.searchResultTerm(FunctionalOperationContract contract,
UseOperationContractRule.Instantiation inst,
Services services)
Searches the result
Term . |
Copyright © 2003-2019 The KeY-Project.