Class | Description |
---|---|
MergeParamsSpec |
Specification of merge parameters for the creation of
MergeContract s;
this is used by KeYJMLParser . |
MergeRuleUtils |
This class encapsulates static methods used in the MergeRule implementation.
|
MergeRuleUtils.CollectLocationVariablesVisitor |
Visitor for collecting program locations in a Java block.
|
MergeRuleUtils.CollectLocationVariablesVisitorHashSet |
Visitor for collecting program locations in a Java block.
|
MergeRuleUtils.CommonAndSpecificSubformulasResult |
TODO
|
MergeRuleUtils.LocVarReplBranchUniqueMap |
Map for renaming variables to their branch-unique names.
|
MergeRuleUtils.Option<T> |
A simple Scala-like option type: Either Some(value) or None.
|
MergeRuleUtils.Option.None<T> | |
MergeRuleUtils.Option.Some<T> | |
MergeRuleUtils.TermWrapper |
Simple term wrapper for comparing terms modulo renaming.
|
MergeRuleUtils.TermWrapperFactory |
Creates
MergeRuleUtils.TermWrapper objects, thereby ensuring that equal term
wrappers also have equal hash codes. |
SymbolicExecutionState |
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
SymbolicExecutionStateWithProgCnt |
A symbolic execution state with program counter is a triple of a symbolic
state in form of a parallel update, a path condition in form of a JavaDL
formula, and a program counter in form of a JavaDL formula with non-empty
Java Block (and a possible post condition as first, and only, sub term).
|
Exception | Description |
---|---|
MergeRuleUtils.NameAlreadyBoundException |
This exception is thrown by methods to indicate that a name for which it
is requested to register it is already known to the system.
|
MergeRuleUtils.SortNotKnownException |
This exception is thrown by methods to indicate that a given KeY sort is
not known in the current situation.
|