Package | Description |
---|---|
de.uka.ilkd.key.rule.merge.procedures |
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).
|
Copyright © 2003-2019 The KeY-Project.