public final class Modality extends AbstractSortedOperator
Modifier and Type | Field and Description |
---|---|
static Modality |
BOX
The box operator of dynamic logic.
|
static Modality |
BOX_TRANSACTION
A Java Card transaction version of the box modality.
|
static Modality |
DIA
The diamond operator of dynamic logic.
|
static Modality |
DIA_TRANSACTION
A Java Card transaction version of the diamond modality.
|
static Modality |
TOUT
The throughout operator of dynamic logic.
|
static Modality |
TOUT_TRANSACTION
A Java Card transaction version of the throughout modality.
|
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
static Modality |
getModality(java.lang.String str)
Returns a modality corresponding to a string
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
boolean |
terminationSensitive()
Whether this modality is termination sensitive,
i.e., it is a "diamond-kind" modality.
|
java.lang.String |
toString() |
boolean |
transaction()
Whether this is a transaction modality
|
void |
validTopLevelException(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.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel, validTopLevelException
public static final Modality DIA
public static final Modality BOX
public static final Modality DIA_TRANSACTION
public static final Modality BOX_TRANSACTION
public static final Modality TOUT
public static final Modality TOUT_TRANSACTION
public static Modality getModality(java.lang.String str)
str
- name of the modality to returnpublic boolean terminationSensitive()
public boolean transaction()
protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.