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.proof.init;
012:
013: import de.uka.ilkd.key.java.JavaInfo;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.TermBuilder;
018: import de.uka.ilkd.key.logic.op.LogicVariable;
019: import de.uka.ilkd.key.logic.op.ProgramVariable;
020: import de.uka.ilkd.key.logic.op.Quantifier;
021: import de.uka.ilkd.key.logic.sort.AbstractCollectionSort;
022: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
023:
024: /**
025: * Convenience class for creating terms related to the implicit
026: * "created" attribute.
027: * Should possibly be merged into TermBuilder?
028: */
029: public class CreatedAttributeTermFactory {
030: public static final CreatedAttributeTermFactory INSTANCE = new CreatedAttributeTermFactory();
031:
032: private static final TermBuilder TB = TermBuilder.DF;
033:
034: private CreatedAttributeTermFactory() {
035: }
036:
037: /**
038: * Creates the formula "objectTerm.<created> = TRUE".
039: */
040: public Term createCreatedTerm(Services services, Term objectTerm) {
041: JavaInfo javaInfo = services.getJavaInfo();
042: ProgramVariable createdAttribute = javaInfo.getAttribute(
043: ImplicitFieldAdder.IMPLICIT_CREATED, javaInfo
044: .getJavaLangObject());
045: Term createdTerm = TB.dot(objectTerm, createdAttribute);
046:
047: return TB.equals(createdTerm, TB.TRUE(services));
048: }
049:
050: /**
051: * Creates the formula "objectTerm.<created> = TRUE | objectTerm = null"
052: */
053: public Term createCreatedOrNullTerm(Services services,
054: Term objectTerm) {
055: Term objectCreatedTerm = createCreatedTerm(services, objectTerm);
056: Term objectNullTerm = TB.equals(objectTerm, TB.NULL(services));
057: return TB.or(objectCreatedTerm, objectNullTerm);
058: }
059:
060: /**
061: * Creates the formula "objectTerm.<created> = TRUE & objectTerm != null"
062: */
063: public Term createCreatedAndNotNullTerm(Services services,
064: Term objectTerm) {
065: Term objectCreatedTerm = createCreatedTerm(services, objectTerm);
066: Term objectNotNullTerm = TB.not(TB.equals(objectTerm, TB
067: .NULL(services)));
068: return TB.and(objectCreatedTerm, objectNotNullTerm);
069: }
070:
071: private Term createQuantifierTerm(Services services, Quantifier q,
072: LogicVariable[] vars, Term subTerm, boolean nullForbidden) {
073: //create conjunction of guard terms for all variables of a
074: //non-primitive type
075: Term guardConjunctionTerm = TB.tt();
076: for (int i = 0; i < vars.length; i++) {
077: if (!(vars[i].sort() instanceof PrimitiveSort)
078: && !(vars[i].sort() instanceof AbstractCollectionSort)) {
079: Term variableTerm = TB.var(vars[i]);
080: Term guardTerm = (nullForbidden ? createCreatedAndNotNullTerm(
081: services, variableTerm)
082: : createCreatedTerm(services, variableTerm));
083: guardConjunctionTerm = TB.and(guardConjunctionTerm,
084: guardTerm);
085: }
086: }
087:
088: //create guarded quantification
089: Term quantifierTerm;
090: if (q.equals(Quantifier.ALL)) {
091: Term guardedTerm = TB.imp(guardConjunctionTerm, subTerm);
092: quantifierTerm = TB.all(vars, guardedTerm);
093: } else {
094: Term guardedTerm = TB.and(guardConjunctionTerm, subTerm);
095: quantifierTerm = TB.ex(vars, guardedTerm);
096: }
097:
098: return quantifierTerm;
099: }
100:
101: /**
102: * Creates a quantifier term where the quantification only covers
103: * objects which have already been created and which are not null.
104: */
105: public Term createCreatedNotNullQuantifierTerm(Services services,
106: Quantifier q, LogicVariable[] vars, Term subTerm) {
107: return createQuantifierTerm(services, q, vars, subTerm, true);
108: }
109:
110: /**
111: * Creates a quantifier term where the quantification only covers
112: * objects which have already been created and which are not null.
113: */
114: public Term createCreatedNotNullQuantifierTerm(Services services,
115: Quantifier q, LogicVariable var, Term subTerm) {
116: return createCreatedNotNullQuantifierTerm(services, q,
117: new LogicVariable[] { var }, subTerm);
118: }
119: }
|