Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Method and Description |
---|---|
static UseOperationContractRule.Instantiation |
UseOperationContractRule.computeInstantiation(Term focusTerm,
Services services)
Computes instantiation for contract rule on passed focus term.
|
Modifier and Type | Method and Description |
---|---|
static java.util.Map<LocationVariable,LocationVariable> |
UseOperationContractRule.computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
static ImmutableList<Term> |
UseOperationContractRule.computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static ProgramVariable |
UseOperationContractRule.computeResultVar(UseOperationContractRule.Instantiation inst,
TermServices services)
Computes the result variable for this instantiation.
|
static Term |
UseOperationContractRule.computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf)
Returns the correct self term.
|
static ImmutableSet<FunctionalOperationContract> |
UseOperationContractRule.getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services)
Returns the operation contracts which are applicable for the passed instantiation.
|
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.