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: * Created on 23.12.2004
11: */
12: package de.uka.ilkd.key.logic.op;
13:
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16:
17: /**
18: * This compute spec operator is used for computing spec. It is a
19: * non-rigid operator which forces the update simplifier to
20: * stop before and to <strong>not</strong> delete anything.
21: * @author bubel
22: */
23: public class ComputeSpecOp extends Junctor implements NonRigid {
24:
25: /**
26: * @param name
27: * @param arity
28: */
29: ComputeSpecOp() {
30: super (new Name("^"), 1);
31: }
32:
33: public boolean isRigid(Term t) {
34: return false;
35: }
36:
37: }
|