001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: /**
009: *
010: */package de.uka.ilkd.key.proof.mgt;
011:
012: import java.util.HashSet;
013:
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.Sort;
017:
018: /**
019: * represents a class of modalities which are to be treated the same way
020: * by the AbstractMethodLemmaFactory. It provides access to a normal
021: * representative of the class (used to give concrete proof obligations for
022: * the method lemma) and schema modal operators representing the class (used
023: * in the method lemma taclets themselves).
024: *
025: */
026: class ModalityClass {
027:
028: /**
029: * the standard pre-defined classes.
030: */
031: private final static ModalityClass[] DEFAULT_CLASSES = new ModalityClass[] {
032: new ModalityClass(new Modality[] { Op.DIA, Op.DIATRC }),
033: new ModalityClass(new Modality[] { Op.BOX, Op.BOXTRC,
034: Op.TOUTTRC }),
035: new ModalityClass(new Modality[] { Op.BOXTRA, Op.TOUTTRA }) };
036:
037: private ModalOperatorSV schema;
038: private Modality[] modalities;
039:
040: /**
041: * creates a modality class consisting of the given modalities. The first
042: * element of the argument array is the normal representative of the
043: * class.
044: * @param mods the array of modalities seen as one modality class
045: */
046: public ModalityClass(Modality[] mods) {
047: HashSet s = new HashSet();
048: for (int i = 0; i < mods.length; i++) {
049: s.add(mods[i]);
050: }
051: schema = (ModalOperatorSV) SchemaVariableFactory
052: .createOperatorSV(new Name(mods[0].name() + "_schema"),
053: Modality.class, Sort.FORMULA, 1, s);
054: modalities = mods;
055: }
056:
057: /**
058: * returns the normal representative from the pre-defined classes for the
059: * given modality. If not found in the pre-defined classes the argument
060: * is returned
061: */
062: public static Modality getNormReprModality(Modality m) {
063: for (int i = 0; i < DEFAULT_CLASSES.length; i++) {
064: if (DEFAULT_CLASSES[i].containsConcrete(m)) {
065: return DEFAULT_CLASSES[i].getNormRepr();
066: }
067: }
068: return m;
069: }
070:
071: /**
072: * returns the schema operator from the pre-defined classes fitting to the
073: * given modality. Of not found in the pre-defined classes the argument
074: * is returned
075: */
076: public static Operator getSchemaModality(Modality m) {
077: for (int i = 0; i < DEFAULT_CLASSES.length; i++) {
078: if (DEFAULT_CLASSES[i].containsConcrete(m)) {
079: return DEFAULT_CLASSES[i].getSchema();
080: }
081: }
082: return m;
083: }
084:
085: /** returns the schema modal operator representing this modality class */
086: public ModalOperatorSV getSchema() {
087: return schema;
088: }
089:
090: /** returns the normal representative modality of this modality class */
091: public Modality getNormRepr() {
092: return modalities[0];
093: }
094:
095: /** returns true iff the modalities of this class include the given
096: * modality argument */
097: public boolean containsConcrete(Modality mod) {
098: return schema.operators().contains(mod);
099: }
100: }
|