01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic.op.oclop;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.sort.Sort;
16: import de.uka.ilkd.key.logic.sort.oclsort.CollectionSort;
17: import de.uka.ilkd.key.logic.sort.oclsort.OclAnySort;
18: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
19:
20: /**
21: * Represents the OCL operation: collect()
22: */
23: public class OclCollect extends OclCollOpBound {
24:
25: public OclCollect() {
26: super (new Name("$collect"), OclSort.OCLANY,
27: OclSort.COLLECTION_OF_OCLANY);
28: }
29:
30: public Sort sort(Term[] subTerm) {
31: Sort resultSort = null;
32: CollectionSort collSort = (CollectionSort) subTerm[0].sort();
33: OclAnySort exprSort = (OclAnySort) subTerm[1].sort();
34: if (collSort.getCollectionKind() == CollectionSort.SET
35: || collSort.getCollectionKind() == CollectionSort.BAG) {
36: resultSort = CollectionSort.getCollectionSort(
37: CollectionSort.BAG, exprSort);
38: } else {
39: resultSort = CollectionSort.getCollectionSort(
40: CollectionSort.SEQUENCE, exprSort);
41: }
42: return resultSort;
43: }
44:
45: public String toString() {
46: return (name() + ":" + OclSort.BAG_OF_OCLANY);
47: }
48:
49: public String proofToString() {
50: String s = OclSort.BAG_OF_OCLANY + " " + name();
51: s += "(" + OclSort.COLLECTION_OF_OCLANY + "," + OclSort.OCLANY;
52: s += ");\n";
53: return s;
54: }
55: }
|