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: package de.uka.ilkd.key.rule.conditions;
09:
10: import de.uka.ilkd.key.java.Services;
11: import de.uka.ilkd.key.logic.Term;
12: import de.uka.ilkd.key.logic.op.AnonymousUpdate;
13: import de.uka.ilkd.key.logic.op.IUpdateOperator;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16: import de.uka.ilkd.key.rule.VariableConditionAdapter;
17: import de.uka.ilkd.key.rule.inst.SVInstantiations;
18:
19: /**
20: * This conditions checks if the update prefix is empty
21: * and that the instantiation of the sv is the predicate
22: * <tt>inReachableState</tt> maybe proceeded by one Update
23: */
24: public class InReachableStateCondition extends VariableConditionAdapter {
25:
26: final private SchemaVariable inReachableState;
27:
28: public InReachableStateCondition(SchemaVariable sv) {
29: inReachableState = sv;
30: }
31:
32: /**
33: * true if the predicate <tt>inReachableState</tt> is preceeded by one or
34: * no updates
35: */
36: public boolean check(SchemaVariable var, SVSubstitute subst,
37: SVInstantiations svInst, Services services) {
38:
39: if (var != inReachableState)
40: return true;
41:
42: if (!(subst instanceof Term))
43: return false;
44:
45: Term t = (Term) subst;
46:
47: if (t.op() instanceof IUpdateOperator
48: && !(t.op() instanceof AnonymousUpdate)) {
49: t = ((IUpdateOperator) t.op()).target(t);
50: } else {
51: // would otherwise return inReachableState, not wrong but useless
52: return false;
53: }
54:
55: return t.op() == services.getJavaInfo().getInReachableState()
56: && svInst.getUpdateContext().isEmpty();
57: }
58:
59: public String toString() {
60: return "\\isInReachableState(" + inReachableState + ")";
61: }
62:
63: }
|