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: // This file is part of KeY - Integrated Deductive Software Design
09: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: /*
17: * Created on 22.12.2004
18: */
19: package de.uka.ilkd.key.rule.metaconstruct;
20:
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.logic.*;
23: import de.uka.ilkd.key.logic.op.*;
24: import de.uka.ilkd.key.logic.sort.Sort;
25: import de.uka.ilkd.key.rule.MatchConditions;
26: import de.uka.ilkd.key.rule.UpdateSimplifier;
27: import de.uka.ilkd.key.rule.inst.SVInstantiations;
28: import de.uka.ilkd.key.rule.updatesimplifier.Update;
29:
30: /**
31: * Creates an anonymising update for a modifies clause.
32: */
33: public class IntroNewAnonUpdateOp extends AbstractMetaOperator {
34:
35: public IntroNewAnonUpdateOp() {
36: super (new Name("#introNewAnonUpdate"), 3);
37: }
38:
39: /* (non-Javadoc)
40: * @see de.uka.ilkd.key.logic.op.MetaOperator#calculate(de.uka.ilkd.key.logic.Term, de.uka.ilkd.key.rule.inst.SVInstantiations, de.uka.ilkd.key.java.Services)
41: */
42: public Term calculate(Term term, SVInstantiations svInst,
43: Services services) {
44: Term target = term.sub(1);
45: final Term updTerm = term.sub(2);
46:
47: if (!(updTerm.op() instanceof IUpdateOperator))
48: return target;
49:
50: final Update upd = Update.createUpdate(updTerm);
51: final UpdateFactory uf = new UpdateFactory(services,
52: new UpdateSimplifier());
53: return uf.prepend(upd, target);
54: }
55:
56: /* (non-Javadoc)
57: * @see de.uka.ilkd.key.logic.op.Operator#validTopLevel(de.uka.ilkd.key.logic.Term)
58: */
59: public boolean validTopLevel(Term term) {
60: return term.arity() == 3 && term.sub(1).sort() == Sort.FORMULA;
61: }
62:
63: /* (non-Javadoc)
64: * @see de.uka.ilkd.key.logic.op.Operator#sort(de.uka.ilkd.key.logic.Term[])
65: */
66: public Sort sort(Term[] term) {
67: return term[1].sort();
68: }
69:
70: /* (non-Javadoc)
71: * @see de.uka.ilkd.key.logic.op.Operator#isRigid(de.uka.ilkd.key.logic.Term)
72: */
73: public boolean isRigid(Term term) {
74: return false;
75: }
76:
77: /** (non-Javadoc)
78: * by default meta operators do not match anything
79: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
80: */
81: public MatchConditions match(SVSubstitute subst,
82: MatchConditions mc, Services services) {
83: return null;
84: }
85: }
|