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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.parser.ocl;
018:
019: import java.util.HashMap;
020: import java.util.LinkedList;
021: import java.util.List;
022: import java.util.Map;
023:
024: import de.uka.ilkd.key.java.Services;
025: import de.uka.ilkd.key.logic.Name;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermBuilder;
028: import de.uka.ilkd.key.logic.TermFactory;
029: import de.uka.ilkd.key.logic.op.Function;
030: import de.uka.ilkd.key.logic.op.LogicVariable;
031: import de.uka.ilkd.key.logic.op.Op;
032: import de.uka.ilkd.key.logic.sort.Sort;
033: import de.uka.ilkd.key.proof.OpReplacer;
034: import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory;
035: import de.uka.ilkd.key.util.Debug;
036:
037: class OCLPredicativeCollection {
038:
039: private static final String VARNAME_PREFIX = "_oclPC";
040: private static final TermFactory tf = TermFactory.DEFAULT;
041: private static final TermBuilder tb = TermBuilder.DF;
042: private static final CreatedAttributeTermFactory createdFactory = CreatedAttributeTermFactory.INSTANCE;
043: private static final Term falseTerm = tf
044: .createJunctorTerm(Op.FALSE);
045: private static int varCounter;
046:
047: private final LogicVariable var;
048: private final Term restriction;
049:
050: /**
051: * Creates a collection which contains all values of a sort which satisfy
052: * some restriction. (predicative)
053: */
054: protected OCLPredicativeCollection(LogicVariable var,
055: Term restriction) {
056: Debug.assertTrue(restriction.sort() == Sort.FORMULA);
057: this .var = var;
058: this .restriction = restriction;
059: }
060:
061: /**
062: * Creates an empty collection.
063: */
064: protected OCLPredicativeCollection() {
065: this .var = createVar(Sort.ANY);
066: this .restriction = falseTerm;
067: }
068:
069: /**
070: * Creates a collection which contains all values of a sort which are not null.
071: */
072: protected OCLPredicativeCollection(Sort sort, Services services) {
073: this .var = createVar(sort);
074: this .restriction = tb.not(tb.equals(tb.var(this .var), tb
075: .NULL(services)));
076: }
077:
078: /**
079: * Creates a collection which contains a single element.
080: */
081: protected OCLPredicativeCollection(Term element) {
082: this .var = createVar(element.sort());
083: this .restriction = tf.createEqualityTerm(getVarAsTerm(),
084: element);
085: }
086:
087: /**
088: * Creates a collection which contains all integers between a lower and
089: * an upper bound (described by terms of sort int).
090: */
091: protected OCLPredicativeCollection(Term lowerBound,
092: Term upperBound, Function leq) {
093: this .var = createVar(lowerBound.sort());
094: Term lowerTerm = tf.createFunctionTerm(leq, lowerBound,
095: getVarAsTerm());
096: Term upperTerm = tf.createFunctionTerm(leq, getVarAsTerm(),
097: upperBound);
098: this .restriction = tf.createJunctorTermAndSimplify(Op.AND,
099: lowerTerm, upperTerm);
100: }
101:
102: /**
103: * Creates a collection which contains all values reachable from a receiver
104: * term by applying an association with multiplicity > 1 (described by a
105: * predicate).
106: */
107: protected OCLPredicativeCollection(Term recTerm, Function assocFunc) {
108: Debug.assertTrue(assocFunc.sort() == Sort.FORMULA);
109: Debug.assertTrue(assocFunc.arity() == 2);
110: List createdVars = new LinkedList();
111: Term predicateTerm = createPredicateTerm(assocFunc, recTerm,
112: createdVars);
113: Debug.assertTrue(createdVars.size() == 1);
114:
115: this .var = (LogicVariable) createdVars.get(0);
116: this .restriction = predicateTerm;
117: }
118:
119: private static LogicVariable createVar(Sort sort) {
120: return new LogicVariable(
121: new Name(VARNAME_PREFIX + varCounter++), sort);
122: }
123:
124: private static Term createPredicateTerm(Function predicate,
125: Term argTerm,
126: /*out*/List /*LogicVariable*/createdVars) {
127: Debug.assertTrue(predicate.sort() == Sort.FORMULA);
128:
129: //prepare arguments
130: Term[] argTerms = new Term[predicate.arity()];
131: for (int i = 0; i < predicate.arity(); i++) {
132: Sort argSort = predicate.argSort(i);
133: if (argSort.equals(argTerm.sort())) {
134: argTerms[i] = argTerm;
135: } else {
136: LogicVariable lv = createVar(argSort);
137: createdVars.add(lv);
138: argTerms[i] = tf.createVariableTerm(lv);
139: }
140: }
141:
142: //create and return predicate term
143: return tf.createFunctionTerm(predicate, argTerms);
144: }
145:
146: private Term replaceVar(LogicVariable lv1, LogicVariable lv2,
147: Term term) {
148: Map map = new HashMap();
149: map.put(lv1, lv2);
150: OpReplacer or = new OpReplacer(map);
151: return or.replace(term);
152: }
153:
154: private Term getConvertedRestriction(Services services,
155: Term additionalRestriction) {
156: Term andTerm = tf.createJunctorTermAndSimplify(Op.AND,
157: restriction, additionalRestriction);
158: return createdFactory.createCreatedNotNullQuantifierTerm(
159: services, Op.EX, var, andTerm);
160: }
161:
162: protected Sort getSort() {
163: return var.sort();
164: }
165:
166: public LogicVariable getVar() {
167: return var;
168: }
169:
170: public Term getVarAsTerm() {
171: return tf.createVariableTerm(var);
172: }
173:
174: public Term getRestriction() {
175: return restriction;
176: }
177:
178: public String toString() {
179: return "(all " + var + " with " + restriction + ")";
180: }
181:
182: /**
183: * Creates a collection which is a subset of this one.
184: */
185: protected OCLPredicativeCollection narrow(Term additionalRestriction) {
186: Term newRestriction = tf.createJunctorTermAndSimplify(Op.AND,
187: restriction, additionalRestriction);
188: return new OCLPredicativeCollection(var, newRestriction);
189: }
190:
191: /**
192: * Creates a collection which is the union of this one and another one.
193: */
194: protected OCLPredicativeCollection union(OCLCollection c) {
195: Term cRestriction = replaceVar(c.getPredVar(), var, c
196: .getPredicativeRestriction());
197: Term newRestriction = tf.createJunctorTermAndSimplify(Op.OR,
198: restriction, cRestriction);
199: return new OCLPredicativeCollection(var, newRestriction);
200: }
201:
202: /**
203: * Creates a collection containing all elements reachable from this one
204: * by applying an attribute, a method, an association etc. This "navigation"
205: * is described by a "navigate term", which could e.g. be "var.a" or
206: * "var.m()".
207: */
208: protected OCLPredicativeCollection navigate(Services services,
209: Term navigateTerm) {
210: LogicVariable newVar = createVar(navigateTerm.sort());
211: Term newVarTerm = tf.createVariableTerm(newVar);
212: Term equalTerm = tf
213: .createEqualityTerm(newVarTerm, navigateTerm);
214: Term newRestriction = getConvertedRestriction(services,
215: equalTerm);
216:
217: return new OCLPredicativeCollection(newVar, newRestriction);
218: }
219:
220: /**
221: * Creates a collection containing all elements reachable from this one
222: * by applying an association with multiplicity > 1 (described by a
223: * predicate).
224: */
225: protected OCLPredicativeCollection navigate(Services services,
226: Function predicate) {
227: Debug.assertTrue(predicate.sort() == Sort.FORMULA);
228: Debug.assertTrue(predicate.arity() == 2);
229:
230: List createdVars = new LinkedList();
231: Term predicateTerm = createPredicateTerm(predicate,
232: getVarAsTerm(), createdVars);
233: Debug.assertTrue(createdVars.size() == 1);
234: LogicVariable newVar = (LogicVariable) createdVars.get(0);
235:
236: Term newRestriction = getConvertedRestriction(services,
237: predicateTerm);
238: return new OCLPredicativeCollection(newVar, newRestriction);
239: }
240: }
|