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: package de.uka.ilkd.key.rule.metaconstruct;
009:
010: import de.uka.ilkd.key.java.JavaInfo;
011: import de.uka.ilkd.key.java.Services;
012: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
016: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.logic.sort.*;
020: import de.uka.ilkd.key.rule.UpdateSimplifier;
021: import de.uka.ilkd.key.rule.updatesimplifier.ArrayOfAssignmentPair;
022: import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair;
023: import de.uka.ilkd.key.rule.updatesimplifier.Update;
024: import de.uka.ilkd.key.rule.updatesimplifier.UpdateSimplifierTermFactory;
025: import de.uka.ilkd.key.util.Debug;
026:
027: /**
028: * generates the proof obligation establishing that a given state describes
029: * a legal pointer structure, i.e. that serveral system invariants are satisfied, like
030: * no created object references a non-created one.
031: */
032: public class InReachableStatePOBuilder extends TermBuilder {
033:
034: private final UpdateFactory uf;
035: private final Services services;
036: private final Sort intSort;
037: private final ProgramVariable created;
038: private final Term TRUE;
039: private final Term FALSE;
040: private final ProgramVariable arraylength;
041:
042: public InReachableStatePOBuilder(Services services) {
043: uf = new UpdateFactory(services, new UpdateSimplifier());
044: this .services = services;
045: this .intSort = services.getTypeConverter().getIntegerLDT()
046: .targetSort();
047: this .created = services.getJavaInfo().getAttribute(
048: ImplicitFieldAdder.IMPLICIT_CREATED,
049: services.getJavaInfo().getJavaLangObject());
050: this .arraylength = services.getJavaInfo().getArrayLength();
051: this .TRUE = TRUE(services);
052: this .FALSE = FALSE(services);
053: }
054:
055: /**
056: * Generates an optimized proof obligation, which is true if the state
057: * described by update <tt>U</tt> in <tt>updateInReachableState:=U(<tt>inReachableState</tt>)</tt>
058: * leads to a legal pointer structure reachable from the current state.
059: */
060: public Term generatePO(Term updateInReachableState) {
061:
062: if (!(updateInReachableState.op() instanceof IUpdateOperator)) {
063: return updateInReachableState;
064: }
065:
066: final IUpdateOperator updateOp = (IUpdateOperator) updateInReachableState
067: .op();
068: if (updateOp instanceof AnonymousUpdate) {
069: return updateInReachableState;
070: }
071: final Update update = Update
072: .createUpdate(updateInReachableState);
073:
074: ListOfTerm conjunctions = SLListOfTerm.EMPTY_LIST;
075: final ArrayOfAssignmentPair pairs = update
076: .getAllAssignmentPairs();
077:
078: for (int i = 0; i < pairs.size(); i++) {
079: final AssignmentPair pair = pairs.getAssignmentPair(i);
080: final Location loc = pair.location();
081:
082: Term result = null;
083: if (loc instanceof ProgramVariable
084: && loc.sort() != Sort.NULL) {
085: final ProgramVariable pv = (ProgramVariable) loc;
086: if (pv.isStatic()) {
087: if (pv.sort() instanceof ObjectSort) {
088: result = staticFieldLiveRef(update, pair);
089: } else { // all implicit field are currently no reference fields
090: final ObjectSort containerType = (ObjectSort) pv
091: .getContainerType().getSort();
092: ProgramVariable[] implicitFields = new ProgramVariable[] {
093: cErroneous(containerType),
094: cInitialized(containerType),
095: cInInit(containerType),
096: cPrepared(containerType),
097: ntc(containerType) };
098:
099: if (pv == implicitFields[4]) {
100: result = nextToCreateUpdatedSafely(update,
101: pv);
102: } else {
103: // if one of these fields is updated we need an additional axiom
104: boolean additionalAxiom = true;
105: if (pv == implicitFields[0]) {
106: result = classErroneousUpdateIRSConform(
107: update, implicitFields);
108: } else if (pv == implicitFields[1]) {
109: result = classInitializedUpdateIRSConform(
110: update, implicitFields);
111: } else if (pv == implicitFields[2]) {
112: result = classInitInProgressUpdateIRSConform(
113: update, implicitFields);
114: } else {
115: additionalAxiom = false;
116: }
117: if (additionalAxiom) {
118: // in <tt>inReachableState</tt>, if a class is neither initialized, nor inInitialization, nor
119: // erroneous (yes, objects of erroneous classes can exist) than no objects
120: // are created
121: final Term notErroneous = equals(
122: var(implicitFields[0]), FALSE);
123: final Term notInitialized = equals(
124: var(implicitFields[1]), FALSE);
125: final Term notInInit = equals(
126: var(implicitFields[2]), FALSE);
127: final Term ntcIsZero = equals(
128: var(implicitFields[4]),
129: zero(services));
130: result = and(update(update, imp(and(
131: and(notErroneous,
132: notInitialized),
133: notInInit), ntcIsZero)), result);
134: }
135: }
136: }
137: } else {
138: Debug.assertTrue(!pv.isMember());
139: }
140: } else if (loc instanceof AttributeOp) {
141: final ProgramVariable pv = (ProgramVariable) ((AttributeOp) loc)
142: .attribute();
143: final Term refPrefix = ((AttributeOp) loc)
144: .referencePrefix(pair.locationAsTerm());
145:
146: if (refPrefix.sort() != Sort.NULL) {
147: if (loc.sort() instanceof ObjectSort) {
148: final LogicVariable[] vPre = atPre(pair);
149: final Term[] tPre = var(vPre);
150: final Term preAx = preAx(tPre, pair
151: .locationSubs());
152: result = update(update, imp(equals(dot(tPre[0],
153: created), TRUE), createdOrNull(dot(
154: tPre, (AttributeOp) loc))));
155: result = all(vPre, imp(preAx, result));
156: } else if (pv == created) {
157: if (refPrefix.op() instanceof SortDependingFunction
158: && ((SortDependingFunction) refPrefix
159: .op())
160: .getKind()
161: .equals(
162: AbstractSort.OBJECT_REPOSITORY_NAME)) {
163: result = createdInvariantForReposInstance(
164: update, refPrefix);
165: } else {
166: return updateInReachableState;
167: }
168: } else if (pv == arraylength) {
169: result = arrayLengthIsIRSConform(refPrefix,
170: update);
171: }
172: }
173: } else if (loc instanceof ArrayOp) {
174: final Sort elementSort = ((ArraySort) ((ArrayOp) loc)
175: .arraySort()).elementSort();
176: if (elementSort instanceof ObjectSort) {
177: final LogicVariable[] vPre = atPre(pair);
178: final Term[] tPre = var(vPre);
179: final Term preAx = preAx(tPre, pair.locationSubs());
180:
181: // a@pre[i@pre]
182: final Term atPreArrayTerm = array((ArrayOp) loc,
183: tPre);
184:
185: result = update(update, and(imp(equals(dot(tPre[0],
186: created), TRUE),
187: createdOrNull(atPreArrayTerm)),
188: arrayStoreValid(tPre[0], atPreArrayTerm)));
189:
190: result = all(vPre, imp(preAx, result));
191: }
192: }
193: if (result != null) {
194: // take care of quantified updates
195: result = quanUpdateClosure(pair, result);
196:
197: conjunctions = conjunctions.prepend(result);
198: }
199: }
200: conjunctions = conjunctions.prepend(globalInvariants(update));
201: final Term po = conjunction(conjunctions.iterator());
202:
203: // no free variables on top level
204: Debug.assertTrue(po.freeVars().size() == 0);
205:
206: return po;
207: }
208:
209: private Term arrayStoreValid(Term arrayRef, Term arrayValue) {
210: final Function f = (Function) services.getNamespaces()
211: .functions().lookup(new Name("arrayStoreValid"));
212: assert f != null : "ArrayStoreValid predicate not found.";
213: return func(f, arrayRef, arrayValue);
214: }
215:
216: /**
217: * in general an update of the <tt><created></tt> attribute would imply to show a large
218: * formula in order to ensure that the <tt>inReachableState</tt> property is preserved. In case of an update
219: * pair
220: * <tt> T::<get>(idx).<created>=TRUE </tt>
221: * the formula can be drastically reduced to
222: * <code>
223: * U( T::<get>(idx@pre).created = TRUE <->
224: * \exists int i; (i>=0 &
225: * i<T.<nextToCreate> &
226: * T::<get>(i) = T::<get>(idx@pre))
227: * </code>
228: * (otherwise in case of <tt> o.<created>=TRUE </tt> one would need to
229: * create the above formula for any subtype of <tt>o</t>'s static type)
230: *
231: * This case is the most common case one usually gets. Other situations are rather artificially
232: * and likely to be the result of faulty user interaction ;-)
233: *
234: * @param update the Update to be checked
235: * @param t_get the Term T::<get>(idx)
236: * @return the relevant invariant
237: */
238: private Term createdInvariantForReposInstance(Update update,
239: Term t_get) {
240: Term result;
241: final SortDependingFunction get = ((SortDependingFunction) t_get
242: .op());
243: final ObjectSort os = (ObjectSort) get.getSortDependingOn();
244: final LogicVariable lv = new LogicVariable(new Name("i"),
245: intSort);
246:
247: final Term idx = t_get.sub(0);
248: final LogicVariable idxPre = atPre(idx, 0);
249: final Term t_idxPre = var(idxPre);
250:
251: /* pair = (T::<get>(idx).created:=b)
252: <code>
253: U( T::<get>(idx@pre).created = TRUE <->
254: \exists int i; (i>=0 &
255: i<T.<nextToCreate> &
256: T::<get>(i) = T::<get>(idx@pre))
257: </code>
258:
259: */
260: final Term getPreIdx = func(get, t_idxPre);
261:
262: result = equiv(equals(dot(getPreIdx, created), TRUE), ex(lv,
263: and(interval(zero(services), var(lv), var(ntc(os))),
264: equals(func(get, var(lv)), getPreIdx))));
265:
266: return all(idxPre, imp(equals(idx, t_idxPre), update(update,
267: result)));
268: }
269:
270: /**
271: * for each assignment pair of an update a formula is created with the relevant parts
272: * of the system invariants necessary to be shown to be preserved. This method computes
273: * the closure of this formula wrt. quantified updates.
274: *
275: * @param pair the assignment pair used to determine the relevant parts of the
276: * system invariant
277: * @param relevantInvariants the relevant part of the system invariants to be checked
278: * for preserveness
279: * @return the closure of the relvant invariant formula
280: */
281: private Term quanUpdateClosure(final AssignmentPair pair,
282: Term relevantInvariants) {
283: Term closure = relevantInvariants;
284: if (pair.nontrivialGuard()) {
285: closure = imp(pair.guard(), closure);
286: }
287: if (pair.boundVars().size() > 0) {
288: closure = tf.createQuantifierTerm(Op.ALL, pair.boundVars(),
289: closure);
290: }
291: return closure;
292: }
293:
294: /**
295: * conjunction of terms that state global invariants, i.e. which have to be added to
296: * the generated proof obligation in each case and where no optimisation is possible by
297: * disregarding pieces by looking on the assignment pairs
298: * @param update the Update to be checked to preserve <tt>inReachableState</tt>
299: * @return global invariants
300: */
301: private Term globalInvariants(Update update) {
302: return noObjectDeletion(update);
303: }
304:
305: /**
306: * Generates a formula ensuring that an update (U) does not delete a former created
307: * object. This created axiom is as follows:
308: * <code>
309: * \forall Object o; (o.<created> = TRUE -> U o.<created> = TRUE)
310: * </code>
311: * @param update the Update U which is checked for object deletion
312: * @return a formula that evaluates to true if the update does not delete objects
313: */
314: private Term noObjectDeletion(Update update) {
315: final LogicVariable o = new LogicVariable(new Name("o"),
316: services.getJavaInfo().getJavaLangObjectAsSort());
317: final Term o_created = equals(dot(var(o), created), TRUE);
318: return all(o, imp(o_created, update(update, o_created)));
319: }
320:
321: /**
322: * Generates a formula checking that the given static field <tt>T.sv</tt> references <tt>null</tt>
323: * or a created object.
324: * Let
325: * <tt>pair=(T.sv := t)</tt>
326: * the method assumes that loc is a static field of reference type ref (ref != Sort.NULL)
327: * and generates the following formula
328: * <code>
329: * U(T.<initialized>=TRUE -> T.sv.<created>=TRUE | T.sv = null)
330: * </code>
331: * ensuring that the static field is only updated to a living object or null
332: * @param the update U to be checked
333: *
334: * @return a formula that evaluates to true iff the update U does not update the
335: * static field loc to an "illegal" value
336: */
337: private Term staticFieldLiveRef(Update update, AssignmentPair pair) {
338: final ProgramVariable classInit = services.getJavaInfo()
339: .getAttribute(
340: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
341: (((ProgramVariable) pair.location()))
342: .getContainerType());
343: return update(update, imp(equals(var(classInit), TRUE),
344: createdOrNull(pair.locationAsTerm())));
345: }
346:
347: /**
348: * generates a formula that ensures that all ensuring that the updated
349: * field <tt>T.<nextToCreate></tt> still satisfies its invariants
350: * namely that its value
351: * <ul>
352: * <li>remains greater than or equals zero</li>
353: * <li>that all created objects have an index between 0 and T.<nextToCreate> </li>
354: * </ul>
355: * <code>
356: * U ( T.<nextToCreate> >= 0 )
357: * &
358: * -- unoptimized \forall int i; (i>=0 & i < T.<nextToCreate> <-> T::<get>(i).<created>=TRUE)
359: * -- optimized
360: * \forall int i; (i>=T.<nextToCreate> & i < U(T.<nextToCreate>) -> U(T::<get>(i).<created>=TRUE))
361: * )
362: * &
363: * T.<nextToCreate> <= U (T.<nextToCreate>)
364: * </code>
365: * @param update the update to be checked
366: * @param pv the ProgramVariable representing <tt>T.<nextToCreate></tt>
367: * @return a formula that evaluates to true if the update U does not destroy the
368: * system invariants of <tt>T.<nextToCreate></tt>
369: */
370: private Term nextToCreateUpdatedSafely(final Update update,
371: final ProgramVariable pv) {
372: Term result;
373: final ObjectSort os = (ObjectSort) pv.getContainerType()
374: .getSort();
375: final LogicVariable iv = new LogicVariable(new Name("i"),
376: intSort);
377:
378: final Term updatedPV = update(update, var(pv));
379:
380: result = geq(updatedPV, zero(services), services);
381:
382: final Term interval = interval(var(pv), var(iv), updatedPV);
383:
384: result = and(result, all(iv, imp(interval, update(update,
385: equals(dot(func(rep(os), var(iv)), created),
386: TRUE(services))))));
387:
388: result = and(result, leq(var(pv), updatedPV, services));
389:
390: return result;
391: }
392:
393: /**
394: * A class that is marked as erroneous is neither initialized nor is its initialization
395: * in progress.
396: *
397: * If a class is marked erroneous its subclasses are not allowed to be initialized. It is
398: * sufficient to test this property for its direct subclasses. As if
399: * ...TODO
400: *
401: * Additionally: from an <tt>inReachableState</tt> state with a class C marked erroneous, no state in
402: * <tt>inReachableState</tt> is reachable where the same class is not erroneous
403: *
404: * <code>
405: * U(C.<erroneous> = TRUE -> (C.<classInitialized> = FALSE &
406: * C.<initInProgress> = FALSE)
407: * &
408: *
409: * U(C.<erroneous> = TRUE -> for all direct subtypes S of C: AND (S.<initialized> = FALSE) )
410: *
411: * &
412: *
413: * C.<erroneous> = TRUE -> U(C.<erroneous> = TRUE)
414: * </code>
415: * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
416: * @param erroneousField the ProgramVariable representing the static field <erroneous> of
417: * a certain class type
418: * @param implicitClassFields the ProgramVariables for the field
419: * C.<erroneous>, C.<initialized>, C.<initInProgress> and C.<nextToCreate>
420: * (in this order)
421: * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
422: * comforming way
423: */
424: private Term classErroneousUpdateIRSConform(Update update,
425: ProgramVariable[] implicitFields) {
426:
427: final Term classErroneous = equals(var(implicitFields[0]), TRUE);
428:
429: Term result = classFieldUpdateConform(update,
430: implicitFields[0], implicitFields[1],
431: implicitFields[2], null);
432:
433: final KeYJavaType currentType = implicitFields[0]
434: .getContainerType();
435: final ListOfKeYJavaType directSubTypes = getDirectSubtypes(currentType);
436:
437: if (!directSubTypes.isEmpty()) {
438: final IteratorOfKeYJavaType it = directSubTypes.iterator();
439: Term subsNotInit = tt();
440: while (it.hasNext()) {
441: final ProgramVariable subsCInitPV = cInitialized((ObjectSort) it
442: .next().getSort());
443: subsNotInit = and(subsNotInit, equals(var(subsCInitPV),
444: FALSE));
445: }
446: result = and(result, update(update, subsNotInit));
447: }
448:
449: result = and(result, imp(classErroneous, update(update,
450: classErroneous)));
451:
452: return result;
453: }
454:
455: /**
456: * A class that is being initialized is neither initialized nor erroneous.
457: * <code>
458: * U(C.<initInProgress> = TRUE -> (C.<erroneous> = FALSE &
459: * C.<initialized> = FALSE &
460: * C.<prepared> = TRUE)
461: * </code>
462: * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
463: * @param erroneousField the ProgramVariable representing the static field <erroneous> of
464: * a certain class type
465: * @param implicitClassFields the ProgramVariables for the field
466: * C.<erroneous>, C.<initialized>, C.<initInProgress> and C.<nextToCreate>
467: * (in this order)
468: * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
469: * comforming way
470: */
471: private Term classInitInProgressUpdateIRSConform(Update update,
472: ProgramVariable[] implicitFields) {
473:
474: Term result = classFieldUpdateConform(update,
475: implicitFields[2], implicitFields[0],
476: implicitFields[1], implicitFields[3]);
477:
478: return result;
479: }
480:
481: /**
482: * A class that is marked as initialized is neither initialized nor is its initialization
483: * in progress.
484: *
485: * If a class is initialized all its supertypes must be initialized, too. It is sufficient
486: * to look at the direct supertypes as if they are initialized all their supertypes are also
487: * initialized in the prestate (as it has the <tt>inReachableState</tt> property) or their fields have been
488: * updated and the formula ensuring this property for their supertypes will be
489: * (or have been) created when looking at the other assignment pairs of the update)
490: *
491: * Additionally: from an <tt>inReachableState</tt> state with an initialized class C, no state in
492: * <tt>inReachableState</tt> is reachable where the same class is not initialized
493: *
494: * <code>
495: * U(C.<initialized> = TRUE -> (C.<erroneous> = FALSE &
496: * C.<initInProgress> = FALSE &
497: * C.<prepared> = TRUE )
498: * &
499: *
500: * U(C.<initialized> = TRUE -> for all direct supertypes S of C: AND (S.<initialized> = TRUE) )
501: *
502: * &
503: * C.<initialized> = TRUE -> U(C.<initialized> = TRUE)
504: * </code>
505: * @param update the Update describing the new state to be checked for the <tt>inReachableState</tt> property
506: * @param erroneousField the ProgramVariable representing the static field <erroneous> of
507: * a certain class type
508: * @param implicitClassFields the ProgramVariables for the field
509: * C.<erroneous>, C.<initialized>, C.<initInProgress>, C.<prepared> and C.<nextToCreate>
510: * (in this order)
511: * @return a formula that evaluates to true if erroneous has been updated by U in an <tt>inReachableState</tt>
512: * comforming way
513: */
514: private Term classInitializedUpdateIRSConform(Update update,
515: ProgramVariable[] implicitFields) {
516:
517: final Term classInitialized = equals(var(implicitFields[1]),
518: TRUE);
519:
520: Term result = classFieldUpdateConform(update,
521: implicitFields[1], implicitFields[0],
522: implicitFields[2], implicitFields[3]);
523: // direct supertypes
524:
525: final ListOfKeYJavaType directSuperTypes = services
526: .getJavaInfo().getDirectSuperTypes(
527: implicitFields[0].getContainerType());
528:
529: if (!directSuperTypes.isEmpty()) {
530: final IteratorOfKeYJavaType it = directSuperTypes
531: .iterator();
532: Term super TypesInit = tt();
533: while (it.hasNext()) {
534: final ProgramVariable super CInitPV = cInitialized((ObjectSort) it
535: .next().getSort());
536: super TypesInit = and(super TypesInit, equals(
537: var(super CInitPV), TRUE));
538: }
539: result = and(result, update(update, imp(classInitialized,
540: super TypesInit)));
541: }
542:
543: // reachable <tt>inReachableState</tt> state
544: result = and(result, imp(classInitialized, update(update,
545: classInitialized)));
546:
547: return result;
548: }
549:
550: /**
551: * the length attribute of arrays is always creater or equal than zero
552: * <code>
553: * \forall x; ((x = arrayReference & x!=null -> U(x.<created>=TRUE -> x.length >= 0)))
554: * </code>
555: */
556: private Term arrayLengthIsIRSConform(Term arrayReference, Update u) {
557: final LogicVariable preRef = atPre(arrayReference, 0);
558: return all(preRef, imp(and(equals(var(preRef), arrayReference),
559: not(equals(var(preRef), NULL(services)))), update(u,
560: imp(equals(dot(var(preRef), created), TRUE(services)),
561: geq(dot(var(preRef), arraylength),
562: zero(services), services)))));
563: }
564:
565: // helper method for class field pos
566:
567: /**
568: * @param currentType
569: * @return
570: */
571: private ListOfKeYJavaType getDirectSubtypes(
572: final KeYJavaType currentType) {
573: ListOfKeYJavaType directSubTypes = SLListOfKeYJavaType.EMPTY_LIST;
574:
575: final JavaInfo javaInfo = services.getJavaInfo();
576: final ListOfKeYJavaType allSubTypes = javaInfo
577: .getAllSubtypes(currentType);
578:
579: final IteratorOfKeYJavaType subTypes = allSubTypes.iterator();
580: while (subTypes.hasNext()) {
581: final KeYJavaType subtype = subTypes.next();
582: final ListOfKeYJavaType subsDirectSuper = javaInfo
583: .getDirectSuperTypes(subtype);
584: if (subsDirectSuper.contains(currentType)) {
585: directSubTypes = directSubTypes.prepend(subtype);
586: }
587: }
588: return directSubTypes;
589: }
590:
591: private Term classFieldUpdateConform(Update update,
592: ProgramVariable fieldA, ProgramVariable fieldB,
593: ProgramVariable fieldC, ProgramVariable fieldD) {
594:
595: final Term classA = equals(var(fieldA), TRUE);
596: final Term classNotB = equals(var(fieldB), FALSE);
597: final Term classNotC = equals(var(fieldC), FALSE);
598:
599: if (fieldD != null) {
600: return update(update, imp(classA, and(and(classNotB,
601: classNotC), equals(var(fieldD), TRUE))));
602: }
603:
604: return update(update, imp(classA, and(classNotB, classNotC)));
605: }
606:
607: // Helpers to build term
608: private Term conjunction(IteratorOfTerm it) {
609: Term result = tt();
610: while (it.hasNext()) {
611: result = and(result, it.next());
612: }
613: return result;
614: }
615:
616: private Term updateNoSimplification(Update update, Term target) {
617: return UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
618: update.getAllAssignmentPairs(), target);
619: }
620:
621: private Term update(Update update, Term target) {
622: return uf.prepend(update, target);
623: }
624:
625: private Term createdOrNull(final Term t_o_a) {
626: return or(equals(dot(t_o_a, created), TRUE), equals(t_o_a,
627: NULL(services)));
628: }
629:
630: private ProgramVariable ntc(ObjectSort os) {
631: return services.getJavaInfo().getAttribute(
632: ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE, os);
633: }
634:
635: private ProgramVariable cInInit(ObjectSort os) {
636: return services.getJavaInfo().getAttribute(
637: ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS, os);
638: }
639:
640: private ProgramVariable cInitialized(ObjectSort os) {
641: return services.getJavaInfo().getAttribute(
642: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED, os);
643: }
644:
645: private ProgramVariable cPrepared(ObjectSort os) {
646: return services.getJavaInfo().getAttribute(
647: ImplicitFieldAdder.IMPLICIT_CLASS_PREPARED, os);
648: }
649:
650: private ProgramVariable cErroneous(ObjectSort os) {
651: return services.getJavaInfo().getAttribute(
652: ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS, os);
653: }
654:
655: private Term interval(Term lower, Term i, Term upper) {
656: return and(geq(i, lower, services), lt(i, upper, services));
657: }
658:
659: private Function rep(ObjectSort os) {
660: return (Function) ((SortDefiningSymbols) os)
661: .lookupSymbol(AbstractSort.OBJECT_REPOSITORY_NAME);
662: }
663:
664: /** creates an attribute term and takes care of shadowed attributes as well */
665: private Term dot(Term[] subs, AttributeOp op) {
666: return tf.createAttributeTerm(op, subs);
667: }
668:
669: /** creates an array term and takes care of shadowed attributes as well */
670: private Term array(ArrayOp op, Term[] subs) {
671: return tf.createArrayTerm(op, subs);
672: }
673:
674: private Term[] var(LogicVariable[] v) {
675: final Term[] result = new Term[v.length];
676: for (int i = 0; i < result.length; i++) {
677: result[i] = var(v[i]);
678: }
679: return result;
680: }
681:
682: private Term preAx(Term[] t1, Term[] t2) {
683: Term result = tt();
684: for (int i = 0; i < t1.length; i++) {
685: result = and(result, equals(t1[i], t2[i]));
686: }
687: return result;
688: }
689:
690: private LogicVariable atPre(Term t, int idx) {
691: final Name name = new Name(t.sort().name().toString().charAt(0)
692: + "" + idx + "irs");
693: return new LogicVariable(name, t.sort());
694: }
695:
696: private LogicVariable[] atPre(AssignmentPair pair) {
697: final Term[] subs = pair.locationSubs();
698: final LogicVariable[] result = new LogicVariable[subs.length];
699: for (int i = 0; i < result.length; i++) {
700: result[i] = atPre(subs[i], i);
701: }
702: return result;
703: }
704: }
|