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;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Named;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.rule.MatchConditions;
19:
20: /**
21: * All symbols acting as members of a term e.g. logical operators, predicates,
22: * functions, variables etc. have to implement this interface.
23: */
24: public interface Operator extends Named, SVSubstitute {
25:
26: /**
27: * returns the name of the operator
28: * @return name of the operator
29: */
30: Name name();
31:
32: /**
33: * checks whether the top level structure of the given @link Term
34: * is syntactically valid, given the assumption that the top level
35: * operator of the term is the same as this Operator. The
36: * assumption that the top level operator and the term are equal
37: * is NOT checked.
38: * @return true iff the top level structure of
39: * the {@link Term} is valid.
40: */
41: boolean validTopLevel(Term term);
42:
43: /**
44: * determines the sort of the {@link Term} if it would be created using this
45: * Operator as top level operator and the given terms as sub terms. The
46: * assumption that the constructed term would be allowed is not checked.
47: * @param term an array of Term containing the subterms of a (potential)
48: * term with this operator as top level operator
49: * @return sort of the term with this operator as top level operator of the
50: * given substerms
51: */
52: Sort sort(Term[] term);
53:
54: /**
55: * the arity of this operator
56: * @return arity of the Operator as int
57: */
58: int arity();
59:
60: /**
61: * @return true if the value of "term" having this operator as
62: * top-level operator and may not be changed by modalities
63: */
64: boolean isRigid(Term term);
65:
66: /**
67: * tests if this operator (plays role of a template) matches
68: * the given operator with respect to the given match
69: * conditions.
70: * If matching fails <code>null</code> is returned.
71: * @param subst the Operator to match
72: * @param mc the MatchConditions to pay respect to
73: * @param services the Services to access model information
74: * @return the resulting match conditions (e.g. with new added
75: * instantiations of schema variables)
76: */
77: MatchConditions match(SVSubstitute subst, MatchConditions mc,
78: Services services);
79:
80: }
|