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