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.casetool;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.SetAsListOfTerm;
016: import de.uka.ilkd.key.logic.SetOfTerm;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.TermBuilder;
019: import de.uka.ilkd.key.logic.op.Function;
020: import de.uka.ilkd.key.logic.op.LogicVariable;
021: import de.uka.ilkd.key.logic.op.NonRigidFunction;
022: import de.uka.ilkd.key.logic.op.Op;
023: import de.uka.ilkd.key.logic.sort.AbstractCollectionSort;
024: import de.uka.ilkd.key.logic.sort.AbstractNonCollectionSort;
025: import de.uka.ilkd.key.logic.sort.Sort;
026: import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * A UML association.
031: */
032: public class Association {
033: private static final TermBuilder tb = TermBuilder.DF;
034: private static final CreatedAttributeTermFactory createdFactory = CreatedAttributeTermFactory.INSTANCE;
035:
036: private final Name name;
037: private final ListOfAssociationEnd ends;
038: private Function predicate;
039: private Function func1;
040: private Function func2;
041:
042: private SetOfTerm axioms;
043:
044: public Association(Services services, String name,
045: ListOfAssociationEnd ends) {
046: Debug.assertTrue(ends.size() >= 2);
047:
048: if (name == null) {
049: name = "";
050: IteratorOfAssociationEnd it = ends.iterator();
051: while (it.hasNext()) {
052: name += it.next().getRoleName() + "_";
053: }
054: name = name.substring(0, name.length() - 1);
055: }
056:
057: this .name = new Name(name);
058: this .ends = ends;
059:
060: initialiseFunctions(services);
061: buildAxioms(services);
062: }
063:
064: public Association(Services services, ListOfAssociationEnd ends) {
065: this (services, null, ends);
066: }
067:
068: public Association(Services services, String name,
069: AssociationEnd end1, AssociationEnd end2) {
070: this (services, name, SLListOfAssociationEnd.EMPTY_LIST.prepend(
071: end2).prepend(end1));
072: }
073:
074: public Association(Services services, AssociationEnd end1,
075: AssociationEnd end2) {
076: this (services, null, end1, end2);
077: }
078:
079: public Name getName() {
080: return name;
081: }
082:
083: public ListOfAssociationEnd getEnds() {
084: return ends;
085: }
086:
087: public SetOfTerm getAxioms() {
088: return axioms;
089: }
090:
091: public String toString() {
092: return name.toString();
093: }
094:
095: private Sort getSort(Services services, ModelClass modelClass) {
096: return services.getJavaInfo().getKeYJavaType(
097: modelClass.getFullClassName()).getSort();
098: }
099:
100: private void initialiseFunctions(Services services) {
101:
102: Sort[] argSorts = new Sort[ends.size()];
103: IteratorOfAssociationEnd it = ends.iterator();
104: int i = 0;
105: while (it.hasNext()) {
106: argSorts[i++] = getSort(services, it.next().getModelClass());
107: }
108: predicate = new NonRigidFunction(name, Sort.FORMULA, argSorts);
109: services.getNamespaces().functions().add(predicate);
110:
111: if (ends.size() == 2) {
112: AssociationEnd end1 = ends.head();
113: AssociationEnd end2 = ends.tail().head();
114: Sort sort1 = getSort(services, end1.getModelClass());
115: Sort sort2 = getSort(services, end2.getModelClass());
116:
117: //TODO: if there is a qualifier <<ordered>> then SequenceSort
118: // instead of SetSort has to be used.
119: Sort resSort1 = sort1;
120: Sort resSort2 = sort2;
121: if (ends.head().getMultiplicity().getMax() != 1) {
122: resSort1 = ((AbstractNonCollectionSort) sort1)
123: .getSetSort();
124: }
125: if (ends.tail().head().getMultiplicity().getMax() != 1) {
126: resSort2 = ((AbstractNonCollectionSort) sort2)
127: .getSetSort();
128: }
129: func1 = new NonRigidFunction(end2.getRoleName(), resSort2,
130: new Sort[] { sort1 });
131: func2 = new NonRigidFunction(end1.getRoleName(), resSort1,
132: new Sort[] { sort2 });
133: services.getNamespaces().functions().add(func1);
134: services.getNamespaces().functions().add(func2);
135: }
136: }
137:
138: private void buildAxioms(Services services) {
139: axioms = SetAsListOfTerm.EMPTY_SET;
140:
141: Function inc1 = (Function) services.getNamespaces().functions()
142: .lookup(new Name(func1.sort() + "::includes"));
143: Function inc2 = (Function) services.getNamespaces().functions()
144: .lookup(new Name(func2.sort() + "::includes"));
145:
146: LogicVariable a1;
147: LogicVariable a2;
148:
149: Term a2InFunc1;
150: Term a1InFunc2;
151:
152: if (func1.sort() instanceof AbstractCollectionSort
153: & func2.sort() instanceof AbstractCollectionSort) {
154: a1 = new LogicVariable(new Name("a1"),
155: ((AbstractCollectionSort) func1.sort())
156: .elementSort());
157: a2 = new LogicVariable(new Name("a2"),
158: ((AbstractCollectionSort) func2.sort())
159: .elementSort());
160:
161: a2InFunc1 = tb.func(inc1, tb.func(func1, tb.var(a2)), tb
162: .var(a1));
163: a1InFunc2 = tb.func(inc2, tb.func(func2, tb.var(a1)), tb
164: .var(a2));
165: }
166:
167: else if (func1.sort() instanceof AbstractCollectionSort
168: & func2.sort() instanceof AbstractNonCollectionSort) {
169: a1 = new LogicVariable(new Name("a1"),
170: ((AbstractCollectionSort) func1.sort())
171: .elementSort());
172: a2 = new LogicVariable(new Name("a2"), func2.sort());
173:
174: a2InFunc1 = tb.func(inc1, tb.func(func1, tb.var(a2)), tb
175: .var(a1));
176: a1InFunc2 = tb.equals(tb.func(func2, tb.var(a1)), tb
177: .var(a2));
178: }
179:
180: else if (func1.sort() instanceof AbstractNonCollectionSort
181: & func2.sort() instanceof AbstractCollectionSort) {
182: a1 = new LogicVariable(new Name("a1"), func1.sort());
183: a2 = new LogicVariable(new Name("a2"),
184: ((AbstractCollectionSort) func2.sort())
185: .elementSort());
186:
187: a2InFunc1 = tb.equals(tb.func(func1, tb.var(a2)), tb
188: .var(a1));
189: a1InFunc2 = tb.func(inc2, tb.func(func2, tb.var(a1)), tb
190: .var(a2));
191: }
192:
193: else {
194: a1 = new LogicVariable(new Name("a1"), func1.sort());
195: a2 = new LogicVariable(new Name("a2"), func2.sort());
196:
197: a2InFunc1 = tb.equals(tb.func(func1, tb.var(a2)), tb
198: .var(a1));
199: a1InFunc2 = tb.equals(tb.func(func2, tb.var(a1)), tb
200: .var(a2));
201: }
202:
203: Term predTerm;
204:
205: if (predicate.argSort(0) == a1.sort()) {
206: predTerm = tb.func(predicate, tb.var(a1), tb.var(a2));
207: } else {
208: predTerm = tb.func(predicate, tb.var(a2), tb.var(a1));
209: }
210: //Axiom defining relation between func1 and func2
211:
212: Term axiom = createdFactory.createCreatedNotNullQuantifierTerm(
213: services, Op.ALL, new LogicVariable[] { a1, a2 }, tb
214: .equiv(a2InFunc1, a1InFunc2));
215:
216: axioms = axioms.add(axiom);
217:
218: // Axiom defining relation between func1 and pred
219:
220: axiom = createdFactory.createCreatedNotNullQuantifierTerm(
221: services, Op.ALL, new LogicVariable[] { a1, a2 }, tb
222: .equiv(a2InFunc1, predTerm));
223:
224: axioms = axioms.add(axiom);
225:
226: // Axiom defining relation between func2 and pred
227:
228: axiom = createdFactory.createCreatedNotNullQuantifierTerm(
229: services, Op.ALL, new LogicVariable[] { a1, a2 }, tb
230: .equiv(a1InFunc2, predTerm));
231:
232: axioms = axioms.add(axiom);
233:
234: }
235:
236: public Function getPredicate() {
237: return predicate;
238: }
239:
240: public Function getFunction1() {
241: return func1;
242: }
243:
244: public Function getFunction2() {
245: return func2;
246: }
247: }
|