de.uka.ilkd.key.logic.op

Class WarySubstOp

java.lang.Object

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

de.uka.ilkd.key.logic.op.SubstOp

de.uka.ilkd.key.logic.op.WarySubstOp

All Implemented Interfaces:

Named, Operator, SVSubstitute

public final class WarySubstOp
extends SubstOp

Field Summary

Fields

Modifier and Type	Field and Description
static SubstOp	SUBST the wary substitution operator {var<-term}'.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	WarySubstOp(Name name)

Method Summary

Modifier and Type	Method and Description
Term	apply(Term term, TermBuilder tb) Apply this substitution operator to term, which has this operator as top-level operator

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

additionalValidTopLevel, sort

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

SUBST

public static final SubstOp SUBST

the wary substitution operator {var<-term}'. {x<-d}'A(x) means replace all free occurrences of variable x in A with d, however without replacing x with a non-rigid A below modalities

Constructor Detail

WarySubstOp

private WarySubstOp(Name name)

Method Detail

apply

public Term apply(Term term,
                  TermBuilder tb)

Description copied from class: SubstOp

Apply this substitution operator to term, which has this operator as top-level operator

Specified by:

apply in class SubstOp

Parameters:

term - the Term on which to apply the substitution

tb - the TermBuilder to use for term construction