de.uka.ilkd.key.logic.op

Class ModalOperatorSV

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

All Implemented Interfaces:

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

public final class ModalOperatorSV
extends AbstractSV

Schema variable matching modal operators.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<Modality>	modalities the set of modalities this sv can match

Constructor Summary

Constructors

Constructor and Description
ModalOperatorSV(Name name, ImmutableSet<Modality> modalities) creates a new SchemaVariable that is used as placeholder for modal operators.

Method Summary

Modifier and Type	Method and Description
ImmutableSet<Modality>	getModalities() returns an unmodifiable set of operators this schemavariable can match
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

Field Detail

modalities

private final ImmutableSet<Modality> modalities

the set of modalities this sv can match

Constructor Detail

ModalOperatorSV

ModalOperatorSV(Name name,
                ImmutableSet<Modality> modalities)

creates a new SchemaVariable that is used as placeholder for modal operators.

Parameters:

name - the Name of the SchemaVariable

modalities - modal operators matched by this SV

Method Detail

getModalities

public ImmutableSet<Modality> getModalities()

returns an unmodifiable set of operators this schemavariable can match

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.