de.uka.ilkd.key.logic.op

Interface SchemaVariable

All Superinterfaces:

Named, Operator, ParsableVariable, SortedOperator, SVSubstitute

All Known Implementing Classes:

AbstractSV, FormulaSV, ModalOperatorSV, ProgramSV, SkolemTermSV, TermLabelSV, TermSV, UpdateSV, VariableSV

public interface SchemaVariable
extends ParsableVariable

This interface represents the root of a schema variable hierarchy to be express termstructures that match on logical terms. Schema variables are used in Taclets where they act as placeholders for other TermSymbols. The TermSymbols a SchemaVariable is allowed to match is specified by their type and sort.

Method Summary

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

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

Method Detail

isStrict

boolean isStrict()

Returns:

true if the schemavariable has the strict modifier which forces the instantiation to have exactly the same sort as the schemavariable (or if the sv is of generic sort - the instantiation of the generic sort)

proofToString

java.lang.String proofToString()

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