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.op.TermSymbol;
16: import de.uka.ilkd.key.logic.sort.Sort;
17: import de.uka.ilkd.key.logic.sort.oclsort.CollectionSort;
18: import de.uka.ilkd.key.logic.sort.oclsort.OclAnySort;
19: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
20:
21: /**
22: * Represents an OCL Bag.
23: * All OCL collections are built using two list-like
24: * constructors, empty<T>() and insert<T>(elem, collection),
25: * where <T> is either Set, Bag, or Sequence.
26: */
27: public class OclInsertBag extends TermSymbol {
28:
29: public OclInsertBag() {
30: super (new Name("$insert_bag"), OclSort.BAG_OF_OCLANY);
31: }
32:
33: /** @return arity of the Function as int */
34: public int arity() {
35: return 2;
36: }
37:
38: /*
39: * checks if the given term is syntactically valid at its top
40: * level assumed the top level operator were this, i.e. if the
41: * direct subterms can be subterms of a term with this top level
42: * operator, the method returns true. Furthermore, it is checked
43: * that no variables are bound for none of the subterms.
44: * @param the Term to be checked.
45: * @return true iff the given term has
46: * subterms that are suitable for this function.
47: */
48: public boolean validTopLevel(Term term) {
49: if (term.arity() != arity()) {
50: return false;
51: }
52: if (term.varsBoundHere(0).size() != 0
53: || term.varsBoundHere(1).size() != 0) {
54: return false;
55: }
56:
57: /* $insert_set(1, $insert_set(2, $empty)) */
58: if (!(term.sub(1).sort() instanceof CollectionSort)) {
59: return false;
60: }
61: CollectionSort collSort = (CollectionSort) term.sub(1).sort();
62: if (collSort.getCollectionKind() != CollectionSort.BAG) {
63: return false;
64: }
65: if (!term.sub(0).sort().extendsTrans(collSort.getElemSort())) {
66: return false;
67: }
68:
69: return true;
70: }
71:
72: public Sort sort(Term[] subTerm) {
73: OclAnySort elemSort = (OclAnySort) subTerm[0].sort();
74: return CollectionSort.getCollectionSort(CollectionSort.BAG,
75: elemSort);
76: }
77:
78: public String toString() {
79: return (name() + ":" + OclSort.BAG_OF_OCLANY);
80: }
81:
82: public String proofToString() {
83: String s = OclSort.BAG_OF_OCLANY + " " + name();
84: s += "(" + OclSort.OCLANY + "," + OclSort.BAG_OF_OCLANY;
85: s += ");\n";
86: return s;
87: }
88: }
|