de.uka.ilkd.key.logic.op

Class VariableSV

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.VariableSV

All Implemented Interfaces:

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

public final class VariableSV
extends AbstractSV
implements QuantifiableVariable

Schema variable that is instantiated with logical variables.

Constructor Summary

Constructors

Constructor and Description
VariableSV(Name name, Sort sort) Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables.

Method Summary

Modifier and Type	Method and Description
java.lang.String	proofToString() Creates a parseable string representation of the declaration of the schema variable.
java.lang.String	toString()

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, validTopLevel, 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.SortedOperator

argSort, argSorts, sort

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

arity, bindVarsAt, isRigid, sort, validTopLevel

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

name

Constructor Detail

VariableSV

VariableSV(Name name,
           Sort sort)

Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables.

Parameters:

name - the Name of the SchemaVariable

sort - the Sort of the SchemaVariable and the matched type

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class AbstractOperator

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