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:
011: package de.uka.ilkd.key.logic.op.oclop;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.op.Function;
015: import de.uka.ilkd.key.logic.op.NonRigidFunction;
016: import de.uka.ilkd.key.logic.op.RigidFunction;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.logic.sort.oclsort.CollectionSort;
019: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
020:
021: public abstract class OclOp {
022:
023: public static final Function INVARIANT = new RigidFunction(
024: new Name("$invariant"), OclSort.OCLINVARIANT, new Sort[] {
025: OclSort.OCLTYPE, OclSort.BOOLEAN });
026:
027: public static final Function CONS_INV = new RigidFunction(new Name(
028: "$cons_inv"), OclSort.SET_OF_OCLINVARIANT, new Sort[] {
029: OclSort.OCLINVARIANT, OclSort.SET_OF_OCLINVARIANT });
030:
031: public static final Function NIL_INV = new RigidFunction(new Name(
032: "$nil_inv"), OclSort.SET_OF_OCLINVARIANT, new Sort[0]);
033:
034: public static final OclInsertSet INSERT_SET = new OclInsertSet();
035: public static final OclInsertBag INSERT_BAG = new OclInsertBag();
036: public static final OclInsertSequence INSERT_SEQUENCE = new OclInsertSequence();
037: public static final OclEmptySet EMPTY_SET = new OclEmptySet();
038: public static final OclEmptyBag EMPTY_BAG = new OclEmptyBag();
039: public static final OclEmptySequence EMPTY_SEQUENCE = new OclEmptySequence();
040: public static final OclIterate ITERATE = new OclIterate();
041: public static final OclQuantifier FOR_ALL = new OclQuantifier(
042: new Name("$forAll"));
043: public static final OclQuantifier EXISTS = new OclQuantifier(
044: new Name("$exists"));
045: public static final OclQuantifier ONE = new OclQuantifier(new Name(
046: "$one"));
047: public static final OclIsUnique IS_UNIQUE = new OclIsUnique();
048: public static final OclSortedBy SORTED_BY = new OclSortedBy();
049: public static final OclAny ANY = new OclAny();
050: public static final OclSetOp INCLUDING = new OclSetOp(new Name(
051: "$including"));
052: public static final OclSetOp EXCLUDING = new OclSetOp(new Name(
053: "$excluding"));
054: public static final OclSequenceOp APPEND = new OclSequenceOp(
055: new Name("$append"));
056: public static final OclSequenceOp PREPEND = new OclSequenceOp(
057: new Name("$prepend"));
058: public static final OclCollectionConversion AS_SET = new OclCollectionConversion(
059: new Name("$asSet"), CollectionSort.SET);
060: public static final OclCollectionConversion AS_BAG = new OclCollectionConversion(
061: new Name("$asBag"), CollectionSort.BAG);
062: public static final OclCollectionConversion AS_SEQUENCE = new OclCollectionConversion(
063: new Name("$asSequence"), CollectionSort.SEQUENCE);
064: public static final OclSubSequence SUB_SEQUENCE = new OclSubSequence();
065: public static final OclSequenceElems AT = new OclSequenceElems(
066: new Name("$at"), 2);
067: public static final OclSequenceElems FIRST = new OclSequenceElems(
068: new Name("$first"), 1);
069: public static final OclSequenceElems LAST = new OclSequenceElems(
070: new Name("$last"), 1);
071: public static final OclIf IF = new OclIf();
072: public static final Function ALL_SUBTYPES = new NonRigidFunction(
073: new Name("$allSubtypes"),
074: //new CollectionSort(CollectionSort.SET,
075: // OclSort.OCLTYPE),
076: OclSort.SET_OF_OCLTYPE, new Sort[] { OclSort.OCLTYPE });
077: public static final Function ALL_INSTANCES = new NonRigidFunction(
078: new Name("$allInstances"),
079: //new CollectionSort(CollectionSort.SET,
080: // OclSort.CLASSIFIER),
081: OclSort.SET_OF_CLASSIFIER, new Sort[] { OclSort.OCLTYPE });
082: public static final OclUnion UNION = new OclUnion();
083: public static final OclIntersection INTERSECTION = new OclIntersection();
084: public static final OclDifference DIFFERENCE = new OclDifference(
085: new Name("$difference"));
086: public static final OclDifference SYMMETRIC_DIFFERENCE = new OclDifference(
087: new Name("$symmetricDifference"));
088: public static final OclSubsetOp SELECT = new OclSubsetOp(new Name(
089: "$select"));
090: public static final OclSubsetOp REJECT = new OclSubsetOp(new Name(
091: "$reject"));
092: public static final OclCollect COLLECT = new OclCollect();
093: public static final Function AND = new RigidFunction(new Name(
094: "$and"), OclSort.BOOLEAN, new Sort[] { OclSort.BOOLEAN,
095: OclSort.BOOLEAN });
096: public static final Function OR = new RigidFunction(
097: new Name("$or"), OclSort.BOOLEAN, new Sort[] {
098: OclSort.BOOLEAN, OclSort.BOOLEAN });
099: public static final Function XOR = new RigidFunction(new Name(
100: "$xor"), OclSort.BOOLEAN, new Sort[] { OclSort.BOOLEAN,
101: OclSort.BOOLEAN });
102: public static final Function IMPLIES = new RigidFunction(new Name(
103: "$implies"), OclSort.BOOLEAN, new Sort[] { OclSort.BOOLEAN,
104: OclSort.BOOLEAN });
105: public static final Function NOT = new RigidFunction(new Name(
106: "$not"), OclSort.BOOLEAN, new Sort[] { OclSort.BOOLEAN });
107: public static final Function EQUALS = new NonRigidFunction(
108: new Name("$equals"), OclSort.BOOLEAN, new Sort[] {
109: OclSort.OCLGENERIC, OclSort.OCLGENERIC });
110: public static final Function NOT_EQUALS = new NonRigidFunction(
111: new Name("$notEquals"), OclSort.BOOLEAN, new Sort[] {
112: OclSort.OCLGENERIC, OclSort.OCLGENERIC });
113: public static final Function OCL_IS_NEW = new NonRigidFunction(
114: new Name("$oclIsNew"), OclSort.BOOLEAN,
115: new Sort[] { OclSort.CLASSIFIER });
116: public static final Function TRUE = new RigidFunction(new Name(
117: "$true"), OclSort.BOOLEAN, new Sort[0]);
118: public static final Function FALSE = new RigidFunction(new Name(
119: "$false"), OclSort.BOOLEAN, new Sort[0]);
120: public static final Function SELF = new NonRigidFunction(new Name(
121: "$self"), OclSort.CLASSIFIER, new Sort[0]);
122: public static final Function INCLUDES = new RigidFunction(new Name(
123: "$includes"), OclSort.BOOLEAN, new Sort[] {
124: OclSort.COLLECTION_OF_OCLANY, OclSort.OCLANY });
125: public static final Function EXCLUDES = new RigidFunction(new Name(
126: "$excludes"), OclSort.BOOLEAN, new Sort[] {
127: OclSort.COLLECTION_OF_OCLANY, OclSort.OCLANY });
128: public static final Function COUNT = new RigidFunction(new Name(
129: "$count"), OclSort.INTEGER, new Sort[] {
130: OclSort.COLLECTION_OF_OCLANY, OclSort.OCLANY });
131: public static final Function INCLUDES_ALL = new RigidFunction(
132: new Name("$includesAll"), OclSort.BOOLEAN, new Sort[] {
133: OclSort.COLLECTION_OF_OCLANY,
134: OclSort.COLLECTION_OF_OCLANY });
135: public static final Function EXCLUDES_ALL = new RigidFunction(
136: new Name("$excludesAll"), OclSort.BOOLEAN, new Sort[] {
137: OclSort.COLLECTION_OF_OCLANY,
138: OclSort.COLLECTION_OF_OCLANY });
139: public static final Function SIZE = new RigidFunction(new Name(
140: "$size"), OclSort.INTEGER,
141: new Sort[] { OclSort.COLLECTION_OF_OCLANY });
142: public static final Function IS_EMPTY = new RigidFunction(new Name(
143: "$isEmpty"), OclSort.BOOLEAN,
144: new Sort[] { OclSort.COLLECTION_OF_OCLANY });
145: public static final Function NOT_EMPTY = new RigidFunction(
146: new Name("$notEmpty"), OclSort.BOOLEAN,
147: new Sort[] { OclSort.COLLECTION_OF_OCLANY });
148: public static final Function SUM = new RigidFunction(new Name(
149: "$sum"), OclSort.REAL,
150: new Sort[] { OclSort.COLLECTION_OF_REAL });
151:
152: public static final Function LESS_THAN = new RigidFunction(
153: new Name("$lessThan"), OclSort.BOOLEAN, new Sort[] {
154: OclSort.REAL, OclSort.REAL });
155: public static final Function LESS_THAN_EQ = new RigidFunction(
156: new Name("$lessThanEq"), OclSort.BOOLEAN, new Sort[] {
157: OclSort.REAL, OclSort.REAL });
158: public static final Function GREATER_THAN = new RigidFunction(
159: new Name("$greaterThan"), OclSort.BOOLEAN, new Sort[] {
160: OclSort.REAL, OclSort.REAL });
161: public static final Function GREATER_THAN_EQ = new RigidFunction(
162: new Name("$greaterThanEq"), OclSort.BOOLEAN, new Sort[] {
163: OclSort.REAL, OclSort.REAL });
164: public static final Function PLUS = new RigidFunction(new Name(
165: "$plus"), OclSort.REAL, new Sort[] { OclSort.REAL,
166: OclSort.REAL });
167: public static final Function MINUS = new RigidFunction(new Name(
168: "$minus"), OclSort.REAL, new Sort[] { OclSort.REAL,
169: OclSort.REAL });
170: public static final Function TIMES = new RigidFunction(new Name(
171: "$times"), OclSort.REAL, new Sort[] { OclSort.REAL,
172: OclSort.REAL });
173: public static final Function DIV_INFIX = new RigidFunction(
174: new Name("$divInfix"), OclSort.REAL, new Sort[] {
175: OclSort.REAL, OclSort.REAL });
176: public static final Function DIV = new RigidFunction(new Name(
177: "$div"), OclSort.INTEGER, new Sort[] { OclSort.INTEGER,
178: OclSort.INTEGER });
179: public static final Function MOD = new RigidFunction(new Name(
180: "$mod"), OclSort.INTEGER, new Sort[] { OclSort.INTEGER,
181: OclSort.INTEGER });
182: public static final Function MIN = new RigidFunction(new Name(
183: "$min"), OclSort.REAL, new Sort[] { OclSort.REAL,
184: OclSort.REAL });
185: public static final Function MAX = new RigidFunction(new Name(
186: "$max"), OclSort.REAL, new Sort[] { OclSort.REAL,
187: OclSort.REAL });
188: public static final Function MINUS_PREFIX = new RigidFunction(
189: new Name("$plus"), OclSort.REAL,
190: new Sort[] { OclSort.REAL });
191: public static final Function ABS = new RigidFunction(new Name(
192: "$abs"), OclSort.REAL, new Sort[] { OclSort.REAL });
193:
194: public static final Function OCL_WRAPPER = new NonRigidFunction(
195: new Name("$OclWrapper"), Sort.FORMULA,
196: new Sort[] { OclSort.OCLGENERIC });
197: }
|