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: package de.uka.ilkd.key.logic;
11:
12: import de.uka.ilkd.key.logic.op.AnonymousUpdate;
13:
14: /**
15: * This is currently only used for anonymous updates,
16: * for general (quantified) updates that is an own class
17: * <code>QuanUpdateTerm</code>
18: */
19: class UpdateTerm extends OpTerm {
20:
21: /**
22: * creates a UpdateTerm
23: * @param op the UpdateOperator
24: * @param subs an array of Term
25: */
26: UpdateTerm(AnonymousUpdate op, Term[] subs) {
27: super (op, subs);
28: }
29:
30: public JavaBlock executableJavaBlock() {
31: return sub(arity() - 1).javaBlock();
32: }
33:
34: /** toString */
35: public String toString() {
36: StringBuffer sb = new StringBuffer("{");
37: sb.append(op().name());
38: sb.append("}");
39: sb.append(sub(arity() - 1));
40: return sb.toString();
41: }
42: }
|