de.uka.ilkd.key.logic.op

Class FormulaSV

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

All Implemented Interfaces:

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

public final class FormulaSV
extends AbstractSV

A schema variable that is used as placeholder for formulas.

Constructor Summary

Constructors

Constructor and Description
FormulaSV(Name name, boolean isRigid)

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

FormulaSV

FormulaSV(Name name,
          boolean isRigid)

Parameters:

name - the name of the SchemaVariable

isRigid - true iff this SV may only match rigid formulas

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.