de.uka.ilkd.key.rule.merge

Class MergeProcedure

java.lang.Object

de.uka.ilkd.key.rule.merge.MergeProcedure

Direct Known Subclasses:

MergeByIfThenElse, MergeIfThenElseAntecedent, MergeTotalWeakening, MergeWithLatticeAbstraction

public abstract class MergeProcedure
extends java.lang.Object

Defines a concrete merge procedure, in particular the result of merging two terms for a given location variable in two Symbolic Execution states.

For example, computing the merge result for a variable x in one state where x is 42 and another one where x is 17, the result could be the update x := c, where c is constrained to be positive by a formula in the returned constraints set.

New merge procedures need to be registered in the list CONCRETE_RULES!

Author:

Dominic Scheurer

See Also:

MergeByIfThenElse, MergeIfThenElseAntecedent, MergeTotalWeakening, MergeWithSignLattice

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	MergeProcedure.ValuesMergeResult Encapsulates the result of a merge of values.

Field Summary

Fields

Modifier and Type	Field and Description
(package private) static ImmutableList<MergeProcedure>	CONCRETE_RULES Concrete merge procedures.

Constructor Summary

Constructors

Constructor and Description
MergeProcedure()

Method Summary

Modifier and Type	Method and Description
abstract boolean	complete() Similar to AbstractBuiltInRuleApp.complete().
static ImmutableList<MergeProcedure>	getMergeProcedures() Returns all registered merge procedures.
static MergeProcedure	getProcedureByName(java.lang.String procName) Returns the merge procedure for the given name.
abstract MergeProcedure.ValuesMergeResult	mergeValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services) Merges two values valueInState1 and valueInState2 of corresponding SE states state1 and state2 to a new value of a merge state.
abstract boolean	requiresDistinguishablePathConditions()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

CONCRETE_RULES

static ImmutableList<MergeProcedure> CONCRETE_RULES

Concrete merge procedures.

Constructor Detail

MergeProcedure

public MergeProcedure()

Method Detail

mergeValuesInStates

public abstract MergeProcedure.ValuesMergeResult mergeValuesInStates(Term v,
                                                                     SymbolicExecutionState state1,
                                                                     Term valueInState1,
                                                                     SymbolicExecutionState state2,
                                                                     Term valueInState2,
                                                                     Term distinguishingFormula,
                                                                     Services services)

Merges two values valueInState1 and valueInState2 of corresponding SE states state1 and state2 to a new value of a merge state.

Parameters:

v - The variable for which the values should be merged

state1 - First SE state.

valueInState1 - Value in state1.

state2 - Second SE state.

valueInState2 - Value in state2.

distinguishingFormula - The user-specified distinguishing formula. May be null (for automatic generation).

services - The services object.

Returns:

The merge result.

complete

public abstract boolean complete()

Similar to AbstractBuiltInRuleApp.complete(). Method was introduced for predicate abstraction (which is not complete if the abstraction predicates are not set).

Returns:

true iff the merge procedure is complete (all neede parameters are set).

requiresDistinguishablePathConditions

public abstract boolean requiresDistinguishablePathConditions()

Returns:

true iff the merge procedure requires distinguishable path conditions. This is usually the case for procedures working with concrete values of input states, and can be false for abstraction methods.

getProcedureByName

public static MergeProcedure getProcedureByName(java.lang.String procName)

Returns the merge procedure for the given name.

Parameters:

procName - Name of the merge procedure.

Returns:

The merge procedure of the given name; null if there is no such procedure.

getMergeProcedures

public static ImmutableList<MergeProcedure> getMergeProcedures()

Returns all registered merge procedures.

Returns: