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: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
009: // Universitaet Koblenz-Landau, Germany
010: // Chalmers University of Technology, Sweden
011: //
012: // The KeY system is protected by the GNU General Public License.
013: // See LICENSE.TXT for details.
014: //
015: //
016:
017: package de.uka.ilkd.key.proof.init;
018:
019: import java.util.HashMap;
020: import java.util.Map;
021:
022: import de.uka.ilkd.key.logic.*;
023: import de.uka.ilkd.key.logic.op.AnonymousUpdate;
024: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
025: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
026: import de.uka.ilkd.key.logic.op.Op;
027: import de.uka.ilkd.key.proof.mgt.Contract;
028: import de.uka.ilkd.key.proof.mgt.Contractable;
029: import de.uka.ilkd.key.rule.UpdateSimplifier;
030: import de.uka.ilkd.key.rule.updatesimplifier.Update;
031: import de.uka.ilkd.key.speclang.ClassInvariant;
032: import de.uka.ilkd.key.speclang.SLTranslationError;
033: import de.uka.ilkd.key.util.Debug;
034:
035: /**
036: * The "CorrectDependsPO" proof obligation.
037: */
038: public class CorrectDependsPO extends AbstractPO {
039:
040: private final SetOfLocationDescriptor dependsClause;
041: private final ClassInvariant inv;
042:
043: //-------------------------------------------------------------------------
044: //constructors
045: //-------------------------------------------------------------------------
046:
047: public CorrectDependsPO(SetOfLocationDescriptor dependsClause,
048: ClassInvariant inv) {
049: super ("CorrectDepends of \"" + inv + "\"", inv.getModelClass());
050: this .dependsClause = dependsClause;
051: this .inv = inv;
052: }
053:
054: //-------------------------------------------------------------------------
055: //local helper methods
056: //-------------------------------------------------------------------------
057:
058: private Update createUpdate(UpdateFactory uf, Map atPreFunctions) {
059: Update result = uf.skip();
060:
061: IteratorOfLocationDescriptor it = dependsClause.iterator();
062: while (it.hasNext()) {
063: LocationDescriptor loc = it.next();
064: Debug.assertTrue(loc instanceof BasicLocationDescriptor);
065: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
066:
067: Term guardTerm = bloc.getFormula();
068: Term locTerm = bloc.getLocTerm();
069:
070: createAtPreFunctionsForTerm(guardTerm, atPreFunctions);
071: createAtPreFunctionsForTerm(locTerm, atPreFunctions);
072:
073: Term[] subTermsAtPre = new Term[locTerm.arity()];
074: ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[locTerm
075: .arity()];
076: for (int i = 0; i < locTerm.arity(); i++) {
077: subTermsAtPre[i] = replaceOps(atPreFunctions, locTerm
078: .sub(i));
079: boundVars[i] = locTerm.varsBoundHere(i);
080: }
081: Term locAtIntermediateTerm = tf.createTerm(locTerm.op(),
082: subTermsAtPre, boundVars, null);
083:
084: Term locAtPreTerm = replaceOps(atPreFunctions, locTerm);
085: Update elementaryUpdate = uf.elementaryUpdate(
086: locAtIntermediateTerm, locAtPreTerm);
087:
088: Term guardAtPreTerm = replaceOps(atPreFunctions, guardTerm);
089: Update guardedUpdate = uf.guard(guardAtPreTerm,
090: elementaryUpdate);
091:
092: Update quantifiedUpdate = guardedUpdate;
093: IteratorOfQuantifiableVariable it2 = locTerm.freeVars()
094: .iterator();
095: while (it2.hasNext()) {
096: quantifiedUpdate = uf.quantify(it2.next(),
097: quantifiedUpdate);
098: }
099:
100: result = uf.sequential(result, quantifiedUpdate);
101: }
102:
103: return result;
104: }
105:
106: //-------------------------------------------------------------------------
107: //methods of ProofOblInput interface
108: //-------------------------------------------------------------------------
109:
110: public void readProblem(ModStrategy mod) throws ProofInputException {
111: //make sure initConfig has been set
112: if (initConfig == null) {
113: throw new IllegalStateException("InitConfig not set.");
114: }
115:
116: //prepare container for @pre-functions
117: Map atPreFunctions = new HashMap();
118:
119: try {
120: //translate invariant
121: Term invTerm = translateInv(inv);
122:
123: //build post term
124: UpdateFactory uf = new UpdateFactory(services,
125: new UpdateSimplifier());
126: Term updateTerm = uf.apply(
127: createUpdate(uf, atPreFunctions), invTerm);
128: AnonymousUpdate au = AnonymousUpdate
129: .getNewAnonymousOperator();
130: Term postTerm = tf
131: .createAnonymousUpdateTerm(au, updateTerm);
132:
133: //build pre term
134: Term atPreDefinitionsTerm = buildAtPreDefinitions(atPreFunctions);
135: Term preTerm = tf.createJunctorTerm(Op.AND,
136: atPreDefinitionsTerm, invTerm);
137:
138: //build implication
139: Term poTerm = tf.createJunctorTerm(Op.IMP, preTerm,
140: postTerm);
141: poTerms = new Term[] { poTerm };
142: } catch (SLTranslationError e) {
143: throw new ProofInputException(e);
144: }
145:
146: //register everything in namespaces
147: registerInNamespaces(atPreFunctions);
148: }
149:
150: public Contractable[] getObjectOfContract() {
151: return new Contractable[0];
152: }
153:
154: public boolean initContract(Contract ct) {
155: return false;
156: }
157:
158: //-------------------------------------------------------------------------
159:
160: protected Term getTerm() {
161: return poTerms[0];
162: }
163: }
|