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.Expression;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
18: import de.uka.ilkd.key.logic.sort.Sort;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: public abstract class ExpressionOperator extends NonRigidFunction {
22:
23: private final Expression expression;
24:
25: public ExpressionOperator(Name name, Sort sort, Expression expr) {
26: super (name, sort, new PrimitiveSort[0]);
27: this .expression = expr;
28: }
29:
30: public Expression expression() {
31: return expression;
32: }
33:
34: public abstract Term resolveExpression(SVInstantiations svInst,
35: Services services);
36:
37: /**
38: * @return true if the value of "term" having this operator as
39: * top-level operator and may not be changed by modalities
40: */
41: public boolean isRigid(Term term) {
42: // perhaps to pessimistic
43: return false;
44: }
45: }
|