|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.Modality
| Modality | | public class Modality extends Op implements NonRigid(Code) | | this class is used to represent a dynamic logic modality like
diamond and box (but also extensions of DL like
preserves and throughout are possible in the future).
For further information see @see PrpgramTerm.
|
| Modality | | Modality(Name name)(Code) | | creates a modal operator with the given name and default arity
Parameters:
name - the Name of the modality |
| Modality | | Modality(Name name, int arity)(Code) | | creates a modal operator with the given name and arity
Parameters:
name - the Name of the modality
Parameters:
arity - the arity of the modality |
| arity | | public int arity()(Code) | | arity of the Diamond operator as int |
| isRigid | | public boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator astop-level operator and may not be changed by modalities |
| sort | | public Sort sort(Term term)(Code) | | for convenience reasons
Sort.FORMULA |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | true if the subterm at postion 0 of the given term has Sort.FORMULA and the arity of the term is 1. |
|
|
|