de.uka.ilkd.key.logic.op

Class TermLabelSV

java.lang.Object

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

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.AbstractSV

de.uka.ilkd.key.logic.op.TermLabelSV

All Implemented Interfaces:

TermLabel, Named, Operator, ParsableVariable, SchemaVariable, SortedOperator, SVSubstitute, Sorted

public final class TermLabelSV
extends AbstractSV
implements SchemaVariable, TermLabel

A schema variable which matches term labels

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	TermLabelSV(Name name)

Method Summary

Modifier and Type	Method and Description
java.lang.Object	getChild(int i) Retrieves the i-th parameter object of this term label.
int	getChildCount() Gets the number of parameters of this term label.
java.lang.String	proofToString() Creates a parseable string representation of the declaration of the schema variable.
java.lang.String	toString()
boolean	validTopLevel(Term term) Checks whether the top level structure of the given @link Term is syntactically valid, given the assumption that the top level operator of the term is the same as this Operator.

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

isStrict, toString

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

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

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

arity, bindVarsAt, isRigid, name, whereToBind

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.logic.op.SchemaVariable

isStrict

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Constructor Detail

TermLabelSV

protected TermLabelSV(Name name)

Method Detail

proofToString

public java.lang.String proofToString()

Description copied from interface: SchemaVariable

Creates a parseable string representation of the declaration of the schema variable.

Specified by:

proofToString in interface SchemaVariable

toString

public java.lang.String toString()

Overrides:

toString in class AbstractOperator

validTopLevel

public boolean validTopLevel(Term term)

Description copied from interface: Operator

Checks whether the top level structure of the given @link Term is syntactically valid, given the assumption that the top level operator of the term is the same as this Operator. The assumption that the top level operator and the term are equal is NOT checked.

Specified by:

validTopLevel in interface Operator

Overrides:

validTopLevel in class AbstractOperator

Returns:

true iff the top level structure of the Term is valid.

getChild

public java.lang.Object getChild(int i)

Description copied from interface: TermLabel

Retrieves the i-th parameter object of this term label.

A term label may have structure, i.e. can be parameterized.

Specified by:

getChild in interface TermLabel

Parameters:

i - the number of the parameter to retrieve ( 0 <= i < getChildCount())

Returns:

the selected parameter

getChildCount

public int getChildCount()

Description copied from interface: TermLabel

Gets the number of parameters of this term label.

Specified by:

getChildCount in interface TermLabel

Returns:

the number of parameters (a non-negative number)