Package | Description |
---|---|
de.uka.ilkd.key.gui.mergerule | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
MergeProcedureCompletion<C extends MergeProcedure>
A completion class for merge procedures.
|
Modifier and Type | Method and Description |
---|---|
static <T extends MergeProcedure> |
MergeProcedureCompletion.create(java.util.function.Function<T,T> completion) |
static <T extends MergeProcedure> |
MergeProcedureCompletion.defaultCompletion() |
<T extends MergeProcedure> |
MergePartnerSelectionDialog.getChosenMergeRule() |
Modifier and Type | Method and Description |
---|---|
static MergeProcedureCompletion<? extends MergeProcedure> |
MergeProcedureCompletion.getCompletionForClass(java.lang.Class<? extends MergeProcedure> cls)
Returns the completion for the given merge procedure class.
|
Modifier and Type | Method and Description |
---|---|
static MergeProcedureCompletion<? extends MergeProcedure> |
MergeProcedureCompletion.getCompletionForClass(java.lang.Class<? extends MergeProcedure> cls)
Returns the completion for the given merge procedure class.
|
Modifier and Type | Method and Description |
---|---|
MergeProcedure |
MergeRuleBuiltInRuleApp.getConcreteRule() |
static MergeProcedure |
MergeProcedure.getProcedureByName(java.lang.String procName)
Returns the merge procedure for the given name.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableList<MergeProcedure> |
MergeProcedure.getMergeProcedures()
Returns all registered merge procedures.
|
Modifier and Type | Method and Description |
---|---|
protected MergeProcedure.ValuesMergeResult |
MergeRule.mergeHeaps(MergeProcedure mergeRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Merges two heaps in a zip-like procedure.
|
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
void |
MergeRuleBuiltInRuleApp.setConcreteRule(MergeProcedure concreteRule) |
Constructor and Description |
---|
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Class and Description |
---|---|
class |
MergeByIfThenElse
Rule that merges two sequents based on the if-then-else construction: If two
locations are assigned different values in the states, the value in the
merged state is chosen based on the path condition.
|
class |
MergeIfThenElseAntecedent
Rule that merges two sequents based on the if-then-else construction: If two
locations are assigned different values in the states, the value in the
merged state is chosen based on the path condition.
|
class |
MergeTotalWeakening
Rule that merges two sequents based on "total" weakening: Replacement of
symbolic state by an update setting every program variable to a fresh Skolem
constant, if the respective program variable does not evaluate to the same
value in both states - in this case, the original value is preserved (->
idempotency).
|
class |
MergeWithLatticeAbstraction
Rule that merges two sequents based on a specified set of abstract domain
lattices.
|
class |
MergeWithPredicateAbstraction
Rule that merges two sequents based on a lattice of user-defined predicates.
|
class |
MergeWithPredicateAbstractionFactory
A factory class for
MergeWithPredicateAbstraction which is itself a
MergeProcedure . |
Modifier and Type | Method and Description |
---|---|
MergeProcedure |
PredicateAbstractionMergeContract.getInstantiatedMergeProcedure(Services services) |
MergeProcedure |
UnparameterizedMergeContract.getInstantiatedMergeProcedure(Services services) |
MergeProcedure |
MergeContract.getInstantiatedMergeProcedure(Services services) |
Modifier and Type | Method and Description |
---|---|
java.lang.Class<? extends MergeProcedure> |
PredicateAbstractionMergeContract.getMergeProcedure() |
java.lang.Class<? extends MergeProcedure> |
UnparameterizedMergeContract.getMergeProcedure() |
java.lang.Class<? extends MergeProcedure> |
MergeContract.getMergeProcedure() |
Constructor and Description |
---|
UnparameterizedMergeContract(MergeProcedure mergeProcedure,
MergePointStatement mps,
KeYJavaType kjt) |
Copyright © 2003-2019 The KeY-Project.