Package | Description |
---|---|
de.uka.ilkd.key.gui.mergerule | |
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
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.
|
de.uka.ilkd.key.util.mergerule | |
org.key_project.ui.interactionlog.model.builtin |
Class and Description |
---|
MergePartner
A
MergePartner consists of a Goal and a
PosInOccurrence ; the PosInOccurrence part indicates the
portion of the sequent in the Goal which represents the symbolic
state-program counter part. |
MergeProcedure
Defines a concrete merge procedure, in particular the result of merging two
terms for a given location variable in two Symbolic Execution states.
|
Class and Description |
---|
MergePartner
A
MergePartner consists of a Goal and a
PosInOccurrence ; the PosInOccurrence part indicates the
portion of the sequent in the Goal which represents the symbolic
state-program counter part. |
Class and Description |
---|
CloseAfterMerge
Rule for closing a partner goal after a merge operation.
|
CloseAfterMergeRuleBuiltInRuleApp
Rule application class for close-after-merge rule applications.
|
MergePartner
A
MergePartner consists of a Goal and a
PosInOccurrence ; the PosInOccurrence part indicates the
portion of the sequent in the Goal which represents the symbolic
state-program counter part. |
MergeProcedure
Defines a concrete merge procedure, in particular the result of merging two
terms for a given location variable in two Symbolic Execution states.
|
MergeProcedure.ValuesMergeResult
Encapsulates the result of a merge of values.
|
MergeRule
Base for implementing merge rules.
|
MergeRule.MergeRuleProgressListener |
Class and Description |
---|
MergeProcedure
Defines a concrete merge procedure, in particular the result of merging two
terms for a given location variable in two Symbolic Execution states.
|
MergeProcedure.ValuesMergeResult
Encapsulates the result of a merge of values.
|
Class and Description |
---|
MergeProcedure
Defines a concrete merge procedure, in particular the result of merging two
terms for a given location variable in two Symbolic Execution states.
|
Class and Description |
---|
MergePartner
A
MergePartner consists of a Goal and a
PosInOccurrence ; the PosInOccurrence part indicates the
portion of the sequent in the Goal which represents the symbolic
state-program counter part. |
Class and Description |
---|
MergeRuleBuiltInRuleApp
Rule application class for merge rule applications.
|
Copyright © 2003-2019 The KeY-Project.