Package | Description |
---|---|
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.rule.merge.procedures |
Class and Description |
---|
MergeWithPredicateAbstraction
Rule that merges two sequents based on a lattice of user-defined predicates.
|
Class and Description |
---|
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.
|
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.
|
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).
|
MergeWithLatticeAbstraction
Rule that merges two sequents based on a specified set of abstract domain
lattices.
|
MergeWithPredicateAbstraction
Rule that merges two sequents based on a lattice of user-defined predicates.
|
MergeWithPredicateAbstractionFactory
A factory class for
MergeWithPredicateAbstraction which is itself a
MergeProcedure . |
ParametricMergeProcedure
A
MergeProcedure like MergeWithPredicateAbstraction which
cannot be applied without parameters being set beforehand. |
UnparametricMergeProcedure
A
MergeProcedure like MergeByIfThenElse which can be applied
without setting any parameters. |
Copyright © 2003-2019 The KeY-Project.