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 java.util.HashSet;
14:
15: import de.uka.ilkd.key.java.Services;
16: import de.uka.ilkd.key.logic.JavaBlock;
17: import de.uka.ilkd.key.logic.Name;
18: import de.uka.ilkd.key.logic.Term;
19: import de.uka.ilkd.key.logic.sort.Sort;
20: import de.uka.ilkd.key.rule.MatchConditions;
21: import de.uka.ilkd.key.util.Debug;
22:
23: public class ModalOperatorSV extends OperatorSV {
24:
25: /** creates a new SchemaVariable. That is used as placeholder for
26: * modal operators.
27: * @param name the Name of the SchemaVariable
28: * @param arity the arity of the modal operators matched by this SV
29: * @param modalities modal operators matched by this SV
30: */
31: ModalOperatorSV(Name name, int arity, HashSet modalities) {
32: super (name, Modality.class, Sort.FORMULA, arity, modalities);
33: }
34:
35: /**
36: * checks whether the top level structure of the given @link Term
37: * is syntactically valid, given the assumption that the top level
38: * operator of the term is the same as this Operator. The
39: * assumption that the top level operator and the term are equal
40: * is NOT checked.
41: * @return true iff the top level structure of
42: * the {@link Term} is valid.
43: */
44: public boolean validTopLevel(Term term) {
45: if (term.arity() != this .arity())
46: return false;
47: boolean result = true;
48: for (int i = 0; i < term.arity(); i++)
49: result = result && term.sub(i).sort().equals(Sort.FORMULA);
50: return result;
51: }
52:
53: /**
54: * @return true if the value of "term" having this operator as
55: * top-level operator and may not be
56: * changed by modalities
57: */
58: public boolean isRigid(Term term) {
59: return (term.javaBlock() == JavaBlock.EMPTY_JAVABLOCK);
60: }
61:
62: /**
63: * (non-Javadoc)
64: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
65: */
66: public MatchConditions match(SVSubstitute subst,
67: MatchConditions mc, Services services) {
68: if (!(subst instanceof Modality)) {
69: Debug
70: .out(
71: "FAILED. ModalitySV matches only modalities (template, orig)",
72: this , subst);
73: return null;
74: }
75: return super .match(subst, mc, services);
76: }
77:
78: // SchemaVariable methods
79:
80: /** toString */
81: public String toString() {
82: return toString(" (modal operator)");
83: }
84:
85: }
|