de.uka.ilkd.key.strategy.feature.findprefix

Class RemoveParentUpdateModifier

java.lang.Object

de.uka.ilkd.key.strategy.feature.findprefix.RemoveParentUpdateModifier

All Implemented Interfaces:

Modifier

public class RemoveParentUpdateModifier
extends java.lang.Object
implements Modifier

If the parent operator of the find term is an update application, then change the position (on which the checkers are applied) to the parent operator. Repeat until parent is no update application.

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
RemoveParentUpdateModifier()

Method Summary

Modifier and Type	Method and Description
PosInOccurrence	modifyPosistion(PosInOccurrence pos) Function which delivers a new position based on pos.

Methods inherited from class java.lang.Object

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

Constructor Detail

RemoveParentUpdateModifier

public RemoveParentUpdateModifier()

Method Detail

modifyPosistion

public PosInOccurrence modifyPosistion(PosInOccurrence pos)

Description copied from interface: Modifier

Function which delivers a new position based on pos.

Specified by:

modifyPosistion in interface Modifier

Parameters:

pos - the position to be modified

Returns:

the (new) position