|
| |
|
| java.lang.Object
 de.uka.ilkd.key.proof.mgt.ModalityClass
| ModalityClass | | class ModalityClass (Code) | | represents a class of modalities which are to be treated the same way
by the AbstractMethodLemmaFactory. It provides access to a normal
representative of the class (used to give concrete proof obligations for
the method lemma) and schema modal operators representing the class (used
in the method lemma taclets themselves).
|
| Constructor Summary | |
| public | ModalityClass(Modality[] mods)
creates a modality class consisting of the given modalities. |
| ModalityClass | | public ModalityClass(Modality[] mods)(Code) | | creates a modality class consisting of the given modalities. The first
element of the argument array is the normal representative of the
class.
Parameters:
mods - the array of modalities seen as one modality class |
| containsConcrete | | public boolean containsConcrete(Modality mod)(Code) | | returns true iff the modalities of this class include the given
modality argument
|
| getNormRepr | | public Modality getNormRepr()(Code) | | returns the normal representative modality of this modality class
|
| getNormReprModality | | public static Modality getNormReprModality(Modality m)(Code) | | returns the normal representative from the pre-defined classes for the
given modality. If not found in the pre-defined classes the argument
is returned
|
| getSchema | | public ModalOperatorSV getSchema()(Code) | | returns the schema modal operator representing this modality class
|
| getSchemaModality | | public static Operator getSchemaModality(Modality m)(Code) | | returns the schema operator from the pre-defined classes fitting to the
given modality. Of not found in the pre-defined classes the argument
is returned
|
|
|
|