de.uka.ilkd.key.rule.merge.procedures

Class MergeWithLatticeAbstraction

java.lang.Object

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

de.uka.ilkd.key.rule.merge.procedures.MergeWithLatticeAbstraction

All Implemented Interfaces:

ParametricMergeProcedure

Direct Known Subclasses:

MergeWithPredicateAbstraction

public abstract class MergeWithLatticeAbstraction
extends MergeProcedure
implements ParametricMergeProcedure

Rule that merges two sequents based on a specified set of abstract domain lattices. If no lattice is specified for a given sort, the rule proceeds such that program variables are unchanged if they are equal in both states and applies the if-then-else construction otherwise.

Author:

Dominic Scheurer

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.merge.MergeProcedure

MergeProcedure.ValuesMergeResult

Constructor Summary

Constructors

Constructor and Description
MergeWithLatticeAbstraction()

Method Summary

Modifier and Type	Method and Description
boolean	complete() Similar to AbstractBuiltInRuleApp.complete().
protected abstract AbstractDomainLattice	getAbstractDomainForSort(Sort s, Services services) Returns the abstract domain lattice for the given sort or null if there has no lattice been specified for that sort.
abstract java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement>	getUserChoices()
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.
boolean	requiresDistinguishablePathConditions()

Methods inherited from class de.uka.ilkd.key.rule.merge.MergeProcedure

getMergeProcedures, getProcedureByName

Methods inherited from class java.lang.Object

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

Constructor Detail

MergeWithLatticeAbstraction

public MergeWithLatticeAbstraction()

Method Detail

getAbstractDomainForSort

protected abstract AbstractDomainLattice getAbstractDomainForSort(Sort s,
                                                                  Services services)

Returns the abstract domain lattice for the given sort or null if there has no lattice been specified for that sort.

Parameters:

s - The sort to return the matching lattice for.

services - The services object.

Returns:

The abstract domain lattice suitable for the given sort. Return null if there is no abstract domain for that sort; in this case, an if-then-else merge will be performed.

getUserChoices

public abstract java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> getUserChoices()

Returns:

Manually chosen lattice elements for program variables.

complete

public boolean complete()

Description copied from class: MergeProcedure

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

Specified by:

complete in class MergeProcedure

Returns:

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

mergeValuesInStates

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

Description copied from class: MergeProcedure

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

Specified by:

mergeValuesInStates in class MergeProcedure

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.

requiresDistinguishablePathConditions

public boolean requiresDistinguishablePathConditions()

Specified by:

requiresDistinguishablePathConditions in class MergeProcedure

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.