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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and 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: package de.uka.ilkd.key.rule.metaconstruct;
017:
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.JavaBlock;
020: import de.uka.ilkd.key.logic.Name;
021: import de.uka.ilkd.key.logic.Term;
022: import de.uka.ilkd.key.logic.TermBuilder;
023: import de.uka.ilkd.key.logic.TermFactory;
024: import de.uka.ilkd.key.logic.UpdateFactory;
025: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
026: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
027: import de.uka.ilkd.key.logic.op.ArrayOp;
028: import de.uka.ilkd.key.logic.op.AttributeOp;
029: import de.uka.ilkd.key.logic.op.Function;
030: import de.uka.ilkd.key.logic.op.IUpdateOperator;
031: import de.uka.ilkd.key.logic.op.IteratorOfLocation;
032: import de.uka.ilkd.key.logic.op.Location;
033: import de.uka.ilkd.key.logic.op.LogicVariable;
034: import de.uka.ilkd.key.logic.op.Op;
035: import de.uka.ilkd.key.logic.op.SetAsListOfLocation;
036: import de.uka.ilkd.key.logic.op.SetOfLocation;
037: import de.uka.ilkd.key.logic.sort.ArraySortImpl;
038: import de.uka.ilkd.key.logic.sort.Sort;
039: import de.uka.ilkd.key.rule.UpdateSimplifier;
040: import de.uka.ilkd.key.rule.inst.SVInstantiations;
041: import de.uka.ilkd.key.rule.updatesimplifier.ArrayOfAssignmentPair;
042: import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair;
043: import de.uka.ilkd.key.rule.updatesimplifier.Update;
044:
045: /* @author Christoph Gladisch
046: * This class is necessary for the following rule :
047: * Gamma |- {u'} phi', Delta Gamma |- {u} phi, u=u' & {u'}phi'<->{u'}phi, Delta
048: * ---------------------------------------------------------
049: * Gamma |- {u} phi, Delta
050: *
051: * this meta construct generates
052: * u=u' & {u'}phi'<->{u'}phi
053: * where
054: * u1=u2 := (obl_f1 & obl_f2 & obl_f3 & ... obl_fn)
055: * and
056: * obl_fi := \forall x1, x2, ... ; ({u1} fi(x1, x2, ...)) = ({u2} fi(x1, x2, ...))
057: *
058: * This rule allowes to substitute updates by equivalent updates "modulo defindness":
059: *
060: */
061: public class MetaEquivalentUpdates extends AbstractMetaOperator {
062: private final static TermFactory tf = TermFactory.DEFAULT;
063: private final static TermBuilder tb = TermBuilder.DF;
064: private UpdateFactory uf;
065: private Services serv;
066:
067: public MetaEquivalentUpdates() {
068: super (new Name("#equivUpdates"), 2);
069: }
070:
071: /**
072: * Determine the sort that the operator <code>op</code> takes as
073: * <code>argNum</code>s argument. Stupid, but class <code>Operator</code>
074: * does not provide a nice API to computer this sort ...
075: */
076: private Sort getArgumentSort(Location op, int argNum) {
077: if (op instanceof AttributeOp) {
078: return getJavaLangObject();
079: } else if (op instanceof ArrayOp) {
080: switch (argNum) {
081: case 0:
082: return ((ArrayOp) op).arraySort();
083: case 1:
084: return serv.getTypeConverter().getIntegerLDT()
085: .getNumberSymbol().sort();
086: }
087: } else if (op instanceof Function) {
088: return ((Function) op).argSort(argNum);
089: }
090:
091: assert false : "Location " + op + " of class " + op.getClass()
092: + " is not supported yet";
093: return null;
094: }
095:
096: /**
097: * obl_fi := \forall x1, x2, ... ; ({u1} fi(x1, x2, ...)) = ({u2} fi(x1, x2, ...))
098: * */
099: private Term eqUpdWithRespectToTerm(Update upd1, Update upd2,
100: Location op) {
101: final Term[] varArray = new Term[op.arity()];
102: //System.out.println("Location as term(" + t.arity() + "):"
103: // + t.toString());
104: for (int j = 0; j < op.arity(); j++) {
105: LogicVariable lv = new LogicVariable(new Name("x" + j),
106: getArgumentSort(op, j));
107: Term vt = tf.createVariableTerm(lv);
108: //System.out.print(" " + vt.toString());
109: varArray[j] = vt;
110: }
111:
112: final Term locWithVars = tf.createTerm(op, varArray,
113: new ArrayOfQuantifiableVariable(),
114: JavaBlock.EMPTY_JAVABLOCK);
115: // System.out.println("Term with free variables: " + locWithVars.toString());
116:
117: final Term u1t = uf.apply(upd1, locWithVars);
118: final Term u2t = uf.apply(upd2, locWithVars);
119:
120: return tb.all(locWithVars.freeVars().toArray(), tb.equals(u1t,
121: u2t));
122: }
123:
124: private Location getUpdatedOp(AssignmentPair ap) {
125: final Location loc = ap.location();
126: if (loc instanceof ArrayOp
127: && loc.sort().extendsTrans(getJavaLangObject())) {
128: // we return the most general ArrayOp, namely the one for
129: // java.lang.Object[]-arrays
130: final Sort javaLangCloneable = serv.getJavaInfo()
131: .getJavaLangCloneableAsSort();
132: final Sort javaIoSerializable = serv.getJavaInfo()
133: .getJavaIoSerializableAsSort();
134: return ArrayOp.getArrayOp(ArraySortImpl.getArraySort(
135: getJavaLangObject(), getJavaLangObject(),
136: javaLangCloneable, javaIoSerializable));
137: }
138: return loc;
139: }
140:
141: private Sort getJavaLangObject() {
142: return serv.getJavaInfo().getJavaLangObjectAsSort();
143: }
144:
145: private SetOfLocation addOperatorsToSet(Update upd,
146: SetOfLocation updatedLocs) {
147: final ArrayOfAssignmentPair pairs = upd.getAllAssignmentPairs();
148: for (int i = 0; i < pairs.size(); i++) {
149: updatedLocs = updatedLocs.add(getUpdatedOp(pairs
150: .getAssignmentPair(i)));
151: }
152: return updatedLocs;
153: }
154:
155: /**
156: * u1=u2 := (obl_f1 & obl_f2 & obl_f3 & ... obl_fn)
157: * and
158: * obl_fi := \forall x1, x2, ... ; ({u1} fi(x1, x2, ...)) = ({u2} fi(x1, x2, ...))
159: */
160: private Term eqivalentUpdates(Update upd1, Update upd2) {
161: SetOfLocation updatedLocs = SetAsListOfLocation.EMPTY_SET;
162:
163: updatedLocs = addOperatorsToSet(upd1, updatedLocs);
164: updatedLocs = addOperatorsToSet(upd2, updatedLocs);
165:
166: // System.out.println("Locations:" + updatedLocs);
167:
168: Term res = tb.tt();
169:
170: final IteratorOfLocation locIt = updatedLocs.iterator();
171: while (locIt.hasNext()) {
172: res = tb.and(res, eqUpdWithRespectToTerm(upd1, upd2, locIt
173: .next()));
174: }
175:
176: return res;
177: }
178:
179: /** {u'}phi<->{u'}phi'*/
180: private Term equivalentSubFormulas(Term u1phi1, Term u2phi2) {
181: final Update upd2 = Update.createUpdate(u2phi2);
182:
183: final Term phi1 = getTarget(u1phi1);
184: final Term phi2 = getTarget(u2phi2);
185:
186: if ((phi1.sort() == Sort.FORMULA) != (phi2.sort() == Sort.FORMULA))
187: return tb.ff();
188:
189: final Term u2phi1 = uf.prepend(upd2, phi1);
190:
191: if (phi1.sort() == Sort.FORMULA)
192: return tb.equiv(u2phi1, u2phi2);
193: else
194: return tb.equals(u2phi1, u2phi2);
195: }
196:
197: private Term getTarget(Term t) {
198: if (t.op() instanceof IUpdateOperator)
199: return ((IUpdateOperator) t.op()).target(t);
200: return t;
201: }
202:
203: /** calculates the resulting term:
204: * u=u' & {u'}phi'<->{u'}phi
205: * where
206: * u1=u2 := (obl_f1 & obl_f2 & obl_f3 & ... obl_fn)
207: * and
208: * obl_fi := \forall x1, x2, ... ; ({u1} fi(x1, x2, ...)) = ({u2} fi(x1, x2, ...))
209: */
210: public Term calculate(Term term, SVInstantiations svInst,
211: Services services) {
212: serv = services;
213: uf = new UpdateFactory(serv, new UpdateSimplifier());
214:
215: final Term u1phi1 = term.sub(0);
216: final Term u2phi2 = term.sub(1);
217: //System.out.println("u1phi1:" + u1phi1.toString());
218: //System.out.println("u2phi2:" + u2phi2.toString());
219: final Update upd1 = Update.createUpdate(u1phi1);
220: final Update upd2 = Update.createUpdate(u2phi2);
221: //System.out.println("upd1:" + upd1.toString());
222: //System.out.println("upd2:" + upd2.toString());
223:
224: final Term u1EqvU2 = eqivalentUpdates(upd1, upd2);
225: //System.out.println("u1EqvU2:" + u1EqvU2.toString());
226: final Term phi1EqvPhi2 = equivalentSubFormulas(u1phi1, u2phi2);
227: //System.out.println("phi1EqvPhi2:" + phi1EqvPhi2.toString());
228:
229: serv = null;
230: uf = null;
231:
232: return tb.and(u1EqvU2, phi1EqvPhi2);
233: }
234:
235: public Sort sort(Term[] term) {
236: return Sort.FORMULA;
237: }
238:
239: public boolean validTopLevel(Term term) {
240: return term.arity() == arity();
241: }
242:
243: }
|