001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic.op;
012:
013: import java.io.ObjectStreamException;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.rule.MatchConditions;
020: import de.uka.ilkd.key.util.Debug;
021:
022: /**
023: * This class contains logical connectives, most of them derive
024: * from this class. If you want to create a term with a connective
025: * that is stored in this class you have to take this one, because
026: * these operators are handled as singleton so that e.g.
027: * these operators are compared using equality on references not on
028: * names.
029: */
030: public abstract class Op implements Operator {
031:
032: // OPERATORS
033: /** the ususal 'negation' operator '-' */
034: public static final Junctor NOT = new Junctor(new Name("not"), 1);
035: /**
036: * the ususal 'and' operator '/\' (be A, B formulae then 'A /\ B'
037: * is true if and only if A is true and B is true
038: */
039: public static final Junctor AND = new Junctor(new Name("and"), 2);
040: /**
041: * the ususal 'or' operator '\/' (be A, B formulae then 'A \/ B'
042: * is true if and only if A is true or B is true
043: */
044: public static final Junctor OR = new Junctor(new Name("or"), 2);
045: /**
046: * the ususal 'implication' operator '->' (be A, B formulae then
047: * 'A -> B' is true if and only if A is false or B is true
048: */
049: public static final Junctor IMP = new Junctor(new Name("imp"), 2);
050: /**
051: * the ususal 'equivalence' operator '<->' (be A, B formulae then
052: * 'A <-> B' is true if and only if A and B have the same truth
053: * value
054: */
055: public static final Equality EQV = new Equality(new Name("equiv"),
056: Sort.FORMULA);
057: /** the ususal 'equality' operator '=' */
058: public static final Equality EQUALS = new Equality(new Name(
059: "equals"));
060: /** the ususal 'forall' operator 'all' (be A a formula then
061: * 'all x.A' is true if and only if for all elements d of the
062: * universe A{x<-d} (x substitued with d) is true */
063: public static final Quantifier ALL = new Quantifier(new Name("all"));
064: /** the ususal 'exists' operator 'ex' (be A a formula then
065: * 'ex x.A' is true if and only if there is at least one elements
066: * d of the universe such that A{x<-d} (x substitued with d) is true */
067: public static final Quantifier EX = new Quantifier(
068: new Name("exist"));
069: /** the diamond operator of dynamic logic. A formula
070: * <alpha;>Phi can be read as after processing the program alpha
071: * there exists a state such that Phi holds. */
072: public static final Modality DIA = new Modality(new Name("diamond"));
073: /** the box operator of dynamic logic. A formula
074: * [alpha;]Phi can be read as 'In all states reachable
075: * processing the program alpha the formula Phi holds'.*/
076: public static final Modality BOX = new Modality(new Name("box"));
077: /** the throughout operator of dynamic logic. A formula
078: * [[alpha;]]Phi can be read as 'In all intermediate states during
079: * processing the program alpha the formula Phi holds'.*/
080: public static final Modality TOUT = new Modality(new Name(
081: "throughout"));
082: /**
083: * Diamond operator used for a transaction that is going to commit
084: */
085: public static final Modality DIATRC = new Modality(new Name(
086: "diamond_trc"));
087: /**
088: * Box operator used for a transaction that is going to commit
089: */
090: public static final Modality BOXTRC = new Modality(new Name(
091: "box_trc"));
092: /**
093: * Throughout operator used for a transaction that is going to commit
094: */
095: public static final Modality TOUTTRC = new Modality(new Name(
096: "throughout_trc"));
097: /**
098: * Diamond operator used for a transaction that is going to abort
099: */
100: public static final Modality DIATRA = new Modality(new Name(
101: "diamond_tra"));
102: /**
103: * Box operator used for a transaction that is going to abort
104: */
105: public static final Modality BOXTRA = new Modality(new Name(
106: "box_tra"));
107: /**
108: * Throughout operator used for a transaction that is going to abort
109: */
110: public static final Modality TOUTTRA = new Modality(new Name(
111: "throughout_tra"));
112: /**
113: * Diamond operator used for a transaction that is suspended
114: */
115: public static final Modality DIASUSP = new Modality(new Name(
116: "diamond_susp"));
117: /**
118: * Box operator used for a transaction that is suspended
119: */
120: public static final Modality BOXSUSP = new Modality(new Name(
121: "box_susp"));
122: /**
123: * Throughout operator used for a transaction that is suspended
124: */
125: public static final Modality TOUTSUSP = new Modality(new Name(
126: "throughout_susp"));
127: /** the wary substitution operator {var<-term}'. {x<-d}'A(x) means
128: * replace all free occurrences of variable x in A with d, however
129: * without replacing x with a non-rigid A below modalities */
130: public static final SubstOp SUBST = new WarySubstOp(new Name(
131: "subst"));
132:
133: /** the true constant */
134: public static final Junctor TRUE = new Junctor(new Name("true"), 0);
135: /** the false constant */
136: public static final Junctor FALSE = new Junctor(new Name("false"),
137: 0);
138: /** the null pointer */
139: public static final Function NULL = new RigidFunction(new Name(
140: "null"), Sort.NULL, new Sort[0]);
141:
142: /** the 'if-then-else' operator */
143: public static final IfThenElse IF_THEN_ELSE = new IfThenElse();
144:
145: /** the 'ifEx-then-else' operator */
146: public static final IfExThenElse IF_EX_THEN_ELSE = new IfExThenElse();
147:
148: /** control operator required for specification computation */
149: public static final Junctor COMPUTE_SPEC_OP = new ComputeSpecOp();
150:
151: protected final Name name;
152:
153: protected Op(Name name) {
154: this .name = name;
155: }
156:
157: protected boolean equalsForResolve(Operator op) {
158: if (op.name().equals(this .name())) {
159: if (op.getClass() == this .getClass()) {
160: if (op instanceof Junctor) {
161: if (((Junctor) op).arity() == ((Junctor) this )
162: .arity()) {
163: return true;
164: }
165: } else {
166: return true;
167: }
168: }
169: }
170: return false;
171: }
172:
173: protected Object readResolve() throws ObjectStreamException {
174:
175: Op[] op = { Op.NOT, Op.AND, Op.OR, Op.IMP, Op.ALL, Op.EX,
176: Op.DIA, Op.BOX, Op.TOUT, Op.DIATRC, Op.BOXTRC,
177: Op.TOUTTRC, Op.DIATRA, Op.BOXTRA, Op.TOUTTRA,
178: Op.DIASUSP, Op.BOXSUSP, Op.TOUTSUSP, Op.SUBST, Op.TRUE,
179: Op.FALSE };
180: for (int i = 0; i < op.length; i++) {
181: if (equalsForResolve(op[i])) {
182: return op[i];
183: }
184: }
185: return this ;
186: }
187:
188: /**
189: * Returns a modality corresponding to a string
190: * @param str name of the modality to return
191: */
192: public static Modality getModality(String str) {
193: return (Modality) Modality.getNameMap().get(str);
194: }
195:
196: public Name name() {
197: return name;
198: }
199:
200: public String toString() {
201: return name().toString();
202: }
203:
204: /**
205: * @return true if the value of "term" having this operator as
206: * top-level operator and may not be changed by modalities
207: */
208: public boolean isRigid(Term term) {
209: return term.hasRigidSubterms();
210: }
211:
212: /**
213: * implements the default operator matching rule which means
214: * that the compared object have to be equal otherwise
215: * matching fails
216: */
217: public MatchConditions match(SVSubstitute subst,
218: MatchConditions mc, Services services) {
219: if (subst == this ) {
220: return mc;
221: }
222: Debug.out(
223: "FAILED. Operators are different(template, candidate)",
224: this, subst);
225: return null;
226: }
227: }
|