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.OclSort;
19:
20: /**
21: * Represents the OCL operation: subSequence()
22: */
23: public class OclSubSequence extends TermSymbol {
24:
25: public OclSubSequence() {
26: super (new Name("$subSequence"), OclSort.SEQUENCE_OF_OCLANY);
27: }
28:
29: /** @return arity of the Function as int */
30: public int arity() {
31: return 3;
32: }
33:
34: /*
35: * checks if the given term is syntactically valid at its top
36: * level assumed the top level operator were this, i.e. if the
37: * direct subterms can be subterms of a term with this top level
38: * operator, the method returns true. Furthermore, it is checked
39: * that no variables are bound for none of the subterms.
40: * @param the Term to be checked.
41: * @return true iff the given term has
42: * subterms that are suitable for this function.
43: */
44: public boolean validTopLevel(Term term) {
45: if (term.arity() != arity()) {
46: return false;
47: }
48: if (!(term.sub(0).sort() instanceof CollectionSort)) {
49: return false;
50: }
51: CollectionSort collSort = (CollectionSort) term.sub(0).sort();
52: if (!(collSort.extendsTrans(OclSort.SEQUENCE_OF_OCLANY))) {
53: return false;
54: }
55: if ((term.sub(1).sort() != OclSort.INTEGER)
56: || (term.sub(2).sort() != OclSort.INTEGER)) {
57: return false;
58: }
59: return true;
60: }
61:
62: public Sort sort(Term[] subTerm) {
63: if (subTerm.length != arity()) {
64: throw new IllegalArgumentException(
65: "Cannot determine sort of "
66: + "invalid term (Wrong arity).");
67: }
68: if (!(subTerm[0].sort() instanceof CollectionSort)) {
69: throw new IllegalArgumentException(
70: "Cannot determine sort of "
71: + "invalid term (First argument must be a Collection).");
72: }
73:
74: OclSort elemSort = ((CollectionSort) subTerm[0].sort())
75: .getElemSort();
76: return CollectionSort.getCollectionSort(
77: CollectionSort.SEQUENCE, elemSort);
78: }
79:
80: public String toString() {
81: return (name() + ":" + OclSort.SEQUENCE_OF_OCLANY);
82: }
83:
84: public String proofToString() {
85: String s = OclSort.SEQUENCE_OF_OCLANY + " " + name();
86: s += "(" + OclSort.SEQUENCE_OF_OCLANY;
87: s += ");\n";
88: return s;
89: }
90: }
|