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.HashMap;
14:
15: import de.uka.ilkd.key.logic.JavaBlock;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.sort.Sort;
19:
20: /** this class is used to represent a dynamic logic modality like
21: * diamond and box (but also extensions of DL like
22: * preserves and throughout are possible in the future).
23: * For further information see @see PrpgramTerm.
24: */
25:
26: public class Modality extends Op implements NonRigid {
27:
28: private static final HashMap nameMap = new HashMap(10);
29:
30: private int arity = 0;
31:
32: /** creates a modal operator with the given name and default arity
33: * @param name the Name of the modality
34: */
35: Modality(Name name) {
36: super (name);
37: this .arity = 1;
38: nameMap.put(name.toString(), this );
39: }
40:
41: /** creates a modal operator with the given name and arity
42: * @param name the Name of the modality
43: * @param arity the arity of the modality
44: */
45: Modality(Name name, int arity) {
46: super (name);
47: this .arity = arity;
48: nameMap.put(name.toString(), this );
49: }
50:
51: public static HashMap getNameMap() {
52: return nameMap;
53: }
54:
55: /** @return Sort.FORMULA
56: */
57: public Sort sort(Term[] term) {
58: return Sort.FORMULA;
59: }
60:
61: /**
62: * for convenience reasons
63: * @return Sort.FORMULA
64: */
65: public Sort sort(Term term) {
66: return Sort.FORMULA;
67: }
68:
69: /** @return true if the subterm at postion 0 of the given term
70: * has Sort.FORMULA and the arity of the term is 1.
71: */
72: public boolean validTopLevel(Term term) {
73: if (term.arity() != 1)
74: return false;
75: return term.sub(0).sort().equals(Sort.FORMULA);
76: }
77:
78: /** @return arity of the Diamond operator as int */
79: public int arity() {
80: return this .arity;
81: }
82:
83: /**
84: * @return true if the value of "term" having this operator as
85: * top-level operator and may not be changed by modalities
86: */
87: public boolean isRigid(Term term) {
88: return super.isRigid(term)
89: && term.javaBlock() == JavaBlock.EMPTY_JAVABLOCK;
90: }
91:
92: }
|