de.uka.ilkd.key.logic.op

Class UpdateApplication

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.UpdateApplication

All Implemented Interfaces:

Named, Operator, SVSubstitute

public final class UpdateApplication
extends AbstractOperator

Singleton class defining a binary operator {u}t that applies updates u to terms, formulas, or other updates t.

Field Summary

Fields

Modifier and Type	Field and Description
static UpdateApplication	UPDATE_APPLICATION

Constructor Summary

Constructors

Modifier	Constructor and Description
private	UpdateApplication()

Method Summary

Modifier and Type	Method and Description
boolean	additionalValidTopLevel(Term term) Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.
static Term	getTarget(Term t)
static Term	getUpdate(Term t)
Sort	sort(ImmutableArray<Term> terms) Determines the sort of the Term if it would be created using this Operator as top level operator and the given terms as sub terms.
static int	targetPos()
static int	updatePos()

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

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

Field Detail

UPDATE_APPLICATION

public static final UpdateApplication UPDATE_APPLICATION

Constructor Detail

UpdateApplication

private UpdateApplication()

Method Detail

sort

public Sort sort(ImmutableArray<Term> terms)

Description copied from interface: Operator

Determines the sort of the Term if it would be created using this Operator as top level operator and the given terms as sub terms. The assumption that the constructed term would be allowed is not checked.

Parameters:

terms - an array of Term containing the subterms of a (potential) term with this operator as top level operator

Returns:

sort of the term with this operator as top level operator of the given substerms

additionalValidTopLevel

public boolean additionalValidTopLevel(Term term)

Description copied from class: AbstractOperator

Allows subclasses to impose custom demands on what constitutes a valid term using the operator represented by the subclass.

Specified by:

additionalValidTopLevel in class AbstractOperator

updatePos

public static int updatePos()

Returns:

the index of the subterm representing the update being applied

getUpdate

public static Term getUpdate(Term t)

Parameters:

t - term with this operator as top level operator

Returns:

the subterm representing the update being applies

targetPos

public static int targetPos()

Returns:

the index of the subterm representing the formula/term/update that the update is applied to

getTarget

public static Term getTarget(Term t)

Parameters:

t - term with this operator as top level operator

Returns:

the subterm representing the formula/term the update is applied to