0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009:
0010: package de.uka.ilkd.key.jml;
0011:
0012: import java.util.*;
0013:
0014: import de.uka.ilkd.key.java.*;
0015: import de.uka.ilkd.key.java.abstraction.Constructor;
0016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0017: import de.uka.ilkd.key.java.declaration.*;
0018: import de.uka.ilkd.key.java.declaration.modifier.Public;
0019: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
0020: import de.uka.ilkd.key.java.expression.operator.New;
0021: import de.uka.ilkd.key.java.recoderext.ClassInitializeMethodBuilder;
0022: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
0023: import de.uka.ilkd.key.java.reference.ExecutionContext;
0024: import de.uka.ilkd.key.java.reference.ReferencePrefix;
0025: import de.uka.ilkd.key.java.reference.TypeRef;
0026: import de.uka.ilkd.key.java.reference.TypeReference;
0027: import de.uka.ilkd.key.java.statement.CatchAllStatement;
0028: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
0029: import de.uka.ilkd.key.java.statement.MethodFrame;
0030: import de.uka.ilkd.key.logic.*;
0031: import de.uka.ilkd.key.logic.op.*;
0032: import de.uka.ilkd.key.logic.sort.ObjectSort;
0033: import de.uka.ilkd.key.logic.sort.Sort;
0034: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
0035: import de.uka.ilkd.key.proof.ProofSaver;
0036: import de.uka.ilkd.key.proof.mgt.JavaModelMethod;
0037: import de.uka.ilkd.key.proof.mgt.ListOfQuantifierPrefixEntry;
0038: import de.uka.ilkd.key.proof.mgt.QuantifierPrefixEntry;
0039: import de.uka.ilkd.key.rule.UpdateSimplifier;
0040: import de.uka.ilkd.key.util.Debug;
0041:
0042: /**
0043: * A generic jml methodspecification used for encapsulating lightweight
0044: * and behavioral methodspecifications
0045: * @deprecated
0046: */
0047: public class JMLMethodSpec extends JMLSpec implements
0048: JMLLemmaMethodSpec, AssignableSpec {
0049:
0050: public static final String EVERYTHING = "everything";
0051:
0052: protected class ModTermKey {
0053:
0054: private boolean desugar, withInv, allInv;
0055:
0056: private int hashValue;
0057: private Term post;
0058:
0059: public ModTermKey(Term post, boolean desugar, boolean withInv,
0060: boolean allInv) {
0061: hashValue = 13 * post.hashCode() + 3 * (desugar ? 1 : 0)
0062: + 5 * (withInv ? 1 : 0) + 7 * (allInv ? 1 : 0);
0063: this .post = post;
0064: this .desugar = desugar;
0065: this .withInv = withInv;
0066: this .allInv = allInv;
0067: }
0068:
0069: public boolean equals(Object o) {
0070: if (!(o instanceof ModTermKey))
0071: return false;
0072: ModTermKey k = (ModTermKey) o;
0073: return k.desugar == desugar && k.withInv == withInv
0074: && k.allInv == allInv && post.equals(k.post);
0075: }
0076:
0077: public int hashCode() {
0078: return hashValue;
0079: }
0080: }
0081:
0082: private static final java.util.Comparator comparator = new java.util.Comparator() {
0083: public int compare(Object o1, Object o2) {
0084: return ("" + o1 + o1.hashCode()).compareTo(("" + o2 + o2
0085: .hashCode()).toString());
0086: }
0087: };
0088:
0089: protected static int excCondCount = 0;
0090: protected static int exceptionVarCount = 0;
0091: protected static Term BOOL_FALSE = null;
0092: protected static Term BOOL_TRUE = null;
0093: protected static int logicVarCount = 0;
0094:
0095: protected static Term nullTerm = null;
0096: protected static int resultVarCount = 0;
0097: private static final UpdateSimplifier simplifier = new UpdateSimplifier();
0098:
0099: private static Term addOldQuantifierHelp(Term a, Term t, Term old,
0100: boolean useQuantifiers) {
0101:
0102: TermBuilder df = TermBuilder.DF;
0103: if (UsefulTools.occursIn(old, a, false)) {
0104: if (useQuantifiers) {
0105: LinkedList l = new LinkedList();
0106: Term t1 = createEqualityTermForOldLV(t, old, l, l, null);
0107: a = df.imp(t1, a);
0108:
0109: if (t.sort() == Sort.FORMULA) {
0110: old = old.sub(0);
0111: }
0112: if (old.op() instanceof ProgramVariable) {
0113: a = UsefulTools.createQuantifierTermWithPV(Op.ALL,
0114: old, (LogicVariable) l.getFirst(), a);
0115: }
0116: } else {
0117: if (t.sort() != Sort.FORMULA
0118: && old.op() instanceof ProgramVariable) {
0119: a = TermFactory.DEFAULT.createUpdateTerm(old, t, a);
0120: } else if (t.sort() == Sort.FORMULA
0121: && old.sub(0).op() instanceof ProgramVariable) {
0122: Term oldVTerm = old.sub(0);
0123: LogicVariable oldlv = new LogicVariable(new Name(
0124: oldVTerm.op().name().toString() + "_lv"),
0125: BOOL_FALSE.sort());
0126:
0127: final Term t1 = df.equals(df.var(oldlv), BOOL_TRUE);
0128: t = df.equiv(t, t1);
0129: a = UsefulTools.createQuantifierTermWithPV(Op.ALL,
0130: oldVTerm, oldlv, df.imp(t, a));
0131: } else {
0132: t = createEqualityTermForOldLV(t, old, null, null,
0133: null);
0134: a = df.imp(t, a);
0135: }
0136: }
0137: }
0138: return a;
0139: }
0140:
0141: /** Applies the transformation tau_update to <code>a</code> iff
0142: * <code>useQuantifiers == false</code> or tau_old otherwise.
0143: */
0144: public static Term addOldQuantifiers(Term a, Map term2old,
0145: boolean useQuantifiers, Namespace params) {
0146: if (a == null)
0147: return a;
0148: final TreeMap param2old = new TreeMap(comparator);
0149: final Set sortedKeys;
0150: if (term2old instanceof SortedMap) {
0151: sortedKeys = term2old.keySet();
0152: } else {
0153: sortedKeys = new TreeSet(comparator);
0154: sortedKeys.addAll(term2old.keySet());
0155: }
0156: final Iterator it = sortedKeys.iterator();
0157: while (it.hasNext()) {
0158: Term t = (Term) it.next();
0159: Term old = (Term) term2old.get(t);
0160: if (params != null && t != null
0161: && params.lookup(t.op().name()) != null
0162: && params.lookup(t.op().name()).equals(t.op())) {
0163: param2old.put(t, old);
0164: } else {
0165: a = addOldQuantifierHelp(a, t, old, useQuantifiers);
0166: }
0167: }
0168: // it is necessary that old-variables associated with parameters are
0169: // updated first because parameters are always implicitely refered to
0170: // in their prestate, which
0171: // can lead to nested old-expressions.
0172: // example: let x be a parameter:
0173: // transforming <P>(... \old(x[i]) ...) to
0174: // {old1:=old2[i]}{old2:=x}<P>(... old1 ...) is obviously wrong
0175: // since x has not yet been assigned to old2 when the update
0176: // {old1:=old2[i]} is applied.
0177: // the correct transformation would be:
0178: // {old2:=x}{old1:=old2[i]}<P>(... old1 ...)
0179: if (params != null && !param2old.isEmpty()) {
0180: a = addOldQuantifiers(a, param2old, useQuantifiers, null);
0181: }
0182: return a;
0183: }
0184:
0185: protected static Term createEqualityTermForOldLV(Term t, Term old,
0186: LinkedList l, LinkedList oldFS, Map lv2old) {
0187: TermFactory tf0 = TermFactory.DEFAULT;
0188: Term lvTerm = null;
0189: Term lvEq = null;
0190: LogicVariable oldlv = null;
0191: if (!(old.op() instanceof ProgramVariable)
0192: || old.sort() == Sort.FORMULA
0193: && !(old.sub(0).op() instanceof ProgramVariable)) {
0194: Term oldFTerm = (t.sort() == Sort.FORMULA ? old.sub(0)
0195: : old);
0196: t = tf0.createEqualityTerm(old, t);
0197: if (oldFS != null) {
0198: if (oldFTerm.op() instanceof ArrayOp) {
0199: oldFS.add(oldFTerm.sub(0).op());
0200: } else {
0201: oldFS.add(oldFTerm.op());
0202: }
0203: }
0204: for (int i = (oldFTerm.op() instanceof ArrayOp) ? 1 : 0; i < oldFTerm
0205: .arity(); i++) {
0206: if (oldFTerm.sub(i).op() instanceof ProgramVariable) {
0207: LogicVariable arglv = new LogicVariable(new Name(
0208: oldFTerm.sub(i).op().name().toString()
0209: + "_lv"), oldFTerm.sub(i).sort());
0210: t = UsefulTools.createQuantifierTermWithPV(Op.ALL,
0211: oldFTerm.sub(i), arglv, t);
0212: } else {
0213: t = tf0.createQuantifierTerm(Op.ALL,
0214: (LogicVariable) oldFTerm.sub(i).op(), t);
0215: }
0216: }
0217: return t;
0218: } else {
0219: if (t.sort() != Sort.FORMULA) {
0220: oldlv = new LogicVariable(new Name("y"
0221: + (logicVarCount++)), t.sort());
0222: l.add(oldlv);
0223: lvEq = lvTerm = tf0.createVariableTerm(oldlv);
0224: } else {
0225: oldlv = new LogicVariable(new Name("y"
0226: + (logicVarCount++)), BOOL_FALSE.sort());
0227: l.add(oldlv);
0228: lvTerm = tf0.createVariableTerm(oldlv);
0229: lvEq = tf0.createEqualityTerm(lvTerm, BOOL_TRUE);
0230: old = old.sub(0);
0231: }
0232: Term t1 = tf0.createEqualityTerm(lvEq, t);
0233: if (lv2old != null)
0234: lv2old.put(lvTerm, old);
0235: return t1;
0236: }
0237: }
0238:
0239: // contains an assignable keyword (like nothing, everithing, ...),
0240: // if one occurd in the specification.
0241: protected String assignableMode = null;
0242: protected SetOfLocationDescriptor assignableVariables = SetAsListOfLocationDescriptor.EMPTY_SET;
0243: private CatchAllStatement catchAllStmt;
0244: //caches the classdeclaration from cSpec
0245: protected TypeDeclaration cd;
0246: protected JMLClassSpec cSpec;
0247: protected Term diverges;
0248: protected KeYJavaType exc;
0249: protected ProgramVariable excVar;
0250: // counter for distinguishing different specs of one method.
0251: protected int id;
0252: //contains the self-variable used in an inherited methodspec.
0253: protected ReferencePrefix inheritedPrefix = null;
0254: protected String inhFrom = "";
0255: private String javaPath;
0256: protected JavaInfo ji;
0257: protected TreeMap lv2old;
0258: private TreeMap lv2const;
0259: protected StatementBlock mBS = null;
0260: protected LinkedHashMap modalityTermForEnsuresCache = new LinkedHashMap();
0261: protected NamespaceSet nss;
0262: private ListOfQuantifierPrefixEntry oldLVs = null;
0263: private ListOfOperator oldFuncSymbols;
0264: protected Namespace params;
0265: private Term pi1 = null;
0266: protected ProgramMethod pm;
0267: private Term post;
0268: private Term pre;
0269: protected ProgramVariable resultVar = null;
0270: /**
0271: * Specification variables (see JML Reference
0272: * Manual, section about Specification Variable Declarations)
0273: */
0274: private ListOfNamed specVars = SLListOfNamed.EMPTY_LIST;
0275:
0276: public Map getLv2Const() {
0277: if (lv2const == null) {
0278: lv2const = new TreeMap(comparator);
0279: }
0280: return lv2const;
0281: }
0282:
0283: protected ProgramVariable self;
0284:
0285: protected Services services;
0286:
0287: protected SetOfSignals signals = SetAsListOfSignals.EMPTY_SET;
0288:
0289: //flag which is set to false iff static initialisation features should be suppressed
0290: protected boolean staticInit = false;
0291:
0292: protected TermBuilder tb;
0293:
0294: protected LinkedHashMap term2old;
0295:
0296: protected JMLMethodSpec() {
0297: }
0298:
0299: public JMLMethodSpec(ProgramMethod pm, Services services,
0300: Namespace params, LinkedHashMap term2old,
0301: JMLClassSpec cSpec, NamespaceSet nss, String javaPath) {
0302: this .pm = pm;
0303: this .progVarNS = new Namespace(cSpec.getProgramVariableNS());
0304: this .funcNS = new Namespace(cSpec.getFunctionNS());
0305: this .cd = cSpec.getClassDeclaration();
0306: this .nss = nss;
0307: this .ji = services.getJavaInfo();
0308: this .services = services;
0309: this .javaPath = javaPath;
0310:
0311: if (nullTerm == null) {
0312: nullTerm = NULL(services);
0313: }
0314: if (BOOL_TRUE == null) {
0315: BOOL_TRUE = TRUE(services);
0316: }
0317: if (BOOL_FALSE == null) {
0318: BOOL_FALSE = FALSE(services);
0319: }
0320: pre = post = tt();
0321:
0322: if (!pm.isStatic()) {
0323: createSelfAndAddImplicitPreconditions(pm, services, cSpec);
0324: }
0325: if (staticInit
0326: && !pm
0327: .getName()
0328: .equals(
0329: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER)) {
0330: addImplicitPreconditionsForStaticMethods(services);
0331:
0332: }
0333:
0334: services.getImplementation2SpecMap().addMethodSpec(this );
0335: diverges = ff();
0336: this .params = params;
0337: this .term2old = term2old;
0338: this .cSpec = cSpec;
0339: exc = services.getJavaInfo().getTypeByClassName(
0340: "java.lang.Exception");
0341: excVar = new LocationVariable(new ProgramElementName("_exc"
0342: + (exceptionVarCount++)), exc);
0343: // progVarNS.add(excVar);
0344: resultVar = makeResultVar();
0345: }
0346:
0347: public void addAssignable(SetOfLocationDescriptor locations) {
0348: assignableVariables = assignableVariables.union(locations);
0349: }
0350:
0351: public SetOfLocationDescriptor getAssignable() {
0352: if (EVERYTHING.equals(getAssignableMode())
0353: && assignableVariables.size() == 0) {
0354: return SetAsListOfLocationDescriptor.EMPTY_SET
0355: .add(EverythingLocationDescriptor.INSTANCE);
0356: }
0357: return assignableVariables;
0358: }
0359:
0360: public void addSignals(KeYJavaType exc, ProgramVariable v, Term cond) {
0361: if (v != null) {
0362: getProgramVariableNS().add(v);
0363: }
0364: signals = signals.add(new Signals(exc, v, cond));
0365: }
0366:
0367: protected JavaBlock catchAllJB(boolean desugar) {
0368: JavaBlock catchAllJB;
0369: if (catchAllStmt == null) {
0370: ParameterDeclaration param = new ParameterDeclaration(
0371: new Modifier[0], new TypeRef(exc),
0372: new VariableSpecification(excVar), false);
0373: catchAllStmt = new CatchAllStatement(makeMBS(), param);
0374: }
0375: if (desugar) {
0376: catchAllJB = JavaBlock
0377: .createJavaBlock((StatementBlock) catchAllStmt
0378: .desugar());
0379: } else {
0380: catchAllJB = JavaBlock.createJavaBlock(new StatementBlock(
0381: catchAllStmt));
0382: }
0383: return catchAllJB;
0384: }
0385:
0386: public void clearModalityTermForEnsuresCache() {
0387: modalityTermForEnsuresCache.clear();
0388: }
0389:
0390: /**
0391: * This is used for modelling specification inheritance for overwritten
0392: * methods.
0393: */
0394: public JMLMethodSpec cloneFor(ProgramMethod pm, JMLClassSpec cSpec) {
0395: if (!isCloneableFor(pm))
0396: return null;
0397: JMLMethodSpec cloned = new JMLMethodSpec();
0398: return cloneForHelper(cloned, pm, cSpec);
0399: }
0400:
0401: public JMLMethodSpec copy() {
0402: JMLMethodSpec copy = new JMLMethodSpec(pm, services, params,
0403: term2old, cSpec, nss, javaPath);
0404: return copyHelper(copy);
0405: }
0406:
0407: protected String toStringHelper(String s) {
0408: return isValid() ? inhFrom
0409: + s
0410: + " for method "
0411: + pm.getName()
0412: + "\nin context "
0413: + cd.getName()
0414: + "\nrequires: "
0415: + (pre == null ? "true" : ProofSaver.printTerm(pre,
0416: services, true).toString())
0417: : "Invalid method spec due to unsupported expression: "
0418: + nsEx.expression();
0419: }
0420:
0421: public String toString() {
0422: return toStringHelper("behavior speccase " + id);
0423: }
0424:
0425: /**
0426: * copys several fields to the incomplete copy <code>copy</copy> of this.
0427: */
0428: protected JMLMethodSpec copyHelper(JMLMethodSpec copy) {
0429: copy.services = services;
0430: copy.progVarNS = progVarNS.copy();
0431: copy.funcNS = funcNS.copy();
0432: copy.tb = tb;
0433: copy.nss = nss;
0434: copy.params = params;
0435: copy.pre = pre;
0436: copy.post = post;
0437: copy.resultVar = resultVar;
0438: copy.assignableMode = getAssignableMode();
0439: copy.diverges = diverges;
0440: copy.term2old = (LinkedHashMap) term2old.clone();
0441: copy.assignableVariables = assignableVariables;
0442: copy.signals = signals;
0443: copy.excVar = excVar;
0444: copy.exc = exc;
0445: copy.specVars = specVars;
0446: copy.nsEx = nsEx;
0447: copy.ji = services.getJavaInfo();
0448: return copy;
0449: }
0450:
0451: protected JMLMethodSpec cloneForHelper(JMLMethodSpec clone,
0452: ProgramMethod pm, JMLClassSpec cSpec) {
0453: clone = copyHelper(clone);
0454: clone.id = id;
0455: clone.inhFrom = inhFrom.equals("") ? "inherited from "
0456: + cd.getName() + " " : inhFrom;
0457: clone.cSpec = cSpec;
0458: //set new prefix
0459: if (!pm.isStatic()) {
0460: if (inheritedPrefix == null) {
0461: clone.inheritedPrefix = getPrefix();
0462: } else {
0463: clone.inheritedPrefix = inheritedPrefix;
0464: }
0465: clone.self = (ProgramVariable) cSpec.getInstancePrefix();
0466: }
0467: clone.cd = cSpec.getClassDeclaration();
0468: KeYJavaType returnType;
0469: if (pm.getTypeReference() == null) {
0470: returnType = ji.getKeYJavaType("void");
0471: } else {
0472: returnType = pm.getTypeReference().getKeYJavaType();
0473: }
0474:
0475: //replace the old arguments by the new ones
0476: Namespace newPNS = UsefulTools.buildParamNamespace(pm
0477: .getMethodDeclaration());
0478: Namespace oldPNS = clone.params;
0479: ArrayOfParameterDeclaration oldParams = this .pm.getParameters();
0480: ArrayOfParameterDeclaration newParams = pm.getParameters();
0481: clone.progVarNS.add(oldPNS.allElements());
0482: clone.params = newPNS;
0483: clone.post = updateParameters(oldParams, newParams, clone.post);
0484: clone.pre = updateParameters(oldParams, newParams, clone.pre);
0485: clone.pm = new ProgramMethod(pm.getMethodDeclaration(), ji
0486: .getKeYJavaType(cSpec.getClassDeclaration()),
0487: returnType, PositionInfo.UNDEFINED);
0488: SetOfSignals si = SetAsListOfSignals.EMPTY_SET;
0489: IteratorOfSignals it = clone.signals.iterator();
0490: while (it.hasNext()) {
0491: Signals s = it.next();
0492: si = si.add(new Signals(s.type(), s.variable(), s
0493: .condition() == null ? null : clone
0494: .updatePrefix(updateParameters(oldParams,
0495: newParams, s.condition()))));
0496: }
0497: clone.signals = si;
0498: Iterator kit = term2old.keySet().iterator();
0499: clone.term2old = new LinkedHashMap();
0500: while (kit.hasNext()) {
0501: Term t = (Term) kit.next();
0502: clone.term2old.put(clone.updatePrefix(updateParameters(
0503: oldParams, newParams, t)), term2old.get(t));
0504: }
0505:
0506: clone.progVarNS.add(cSpec.getProgramVariableNS());
0507: clone.funcNS.add(cSpec.getFunctionNS());
0508:
0509: if (staticInit
0510: && !pm
0511: .getName()
0512: .equals(
0513: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER)
0514: && !(cSpec.getClassDeclaration() instanceof InterfaceDeclaration)) {
0515: ProgramVariable ci = services.getJavaInfo().getAttribute(
0516: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
0517: ji.getKeYJavaType(cSpec.getClassDeclaration()));
0518: if (ci != null) {
0519: clone.addPre(equals(tf.createVariableTerm(ci),
0520: BOOL_TRUE));
0521: }
0522: }
0523: clone.updateAssignableLocations();
0524: clone.javaPath = javaPath;
0525: return clone;
0526: }
0527:
0528: /**
0529: * @param t1 the precondition.
0530: * @param jb the JavaBlock used in the modality.
0531: */
0532: protected Term createDiverges() {
0533: if (diverges != null && !ff().equals(diverges)) {
0534: final Term div = tf.createDiamondTerm(catchAllJB(true),
0535: tt());
0536: final Term divPre = updatePrefix(not(diverges));
0537: return imp(divPre, div);
0538: }
0539: return tt();
0540: }
0541:
0542: /** Creates a DL formula from this method specification:
0543: * ((pre & inv) -> [{methodbody}]post) & ((pre & inv & !diverges) -> <{methodbody}>post)
0544: * (This is the DL formula that is needed for an "ensured postcondition
0545: * proofobligation")
0546: * @param withInvariant: iff true the invariant of the containing type
0547: * is added to the postcondition which is needed for JMLPostAndInvPOs
0548: * created by JMLMethodContracts.
0549: * @param allInvariants: iff true all existing invariants for every
0550: * existing type are added to the precondition (and postcondition if
0551: * withInvariant is also true).
0552: */
0553: public Term createDLFormula(boolean withPostInvariant,
0554: boolean allInvariants) {
0555: Term result, t1, t2;
0556: result = t2 = null;
0557: t1 = getPre();
0558: if (allInvariants
0559: && !services.getImplementation2SpecMap().getModifiers(
0560: pm).contains("helper")) {
0561: Term ai = UsefulTools.allInvariants(services
0562: .getImplementation2SpecMap());
0563: t1 = UsefulTools.makeConjunction(t1, ai);
0564: } else {
0565: t1 = cSpec.addClassSpec2Pre(t1, pm, cSpec);
0566: }
0567: t2 = getPost();
0568: if (t2 == null) {
0569: result = createModalityTermForEnsures(tt(), true,
0570: withPostInvariant, allInvariants);
0571: } else {
0572: result = createModalityTermForEnsures(t2, true,
0573: withPostInvariant, allInvariants);
0574: }
0575: if (diverges != null && !ff().equals(diverges)) {
0576: result = and(result, createDiverges());
0577: }
0578: if (t1 != null) {
0579: result = imp(t1, result);
0580: }
0581: result = addOldQuantifiers(result, term2old, false, params);
0582:
0583: if (cSpec != null) {
0584: result = addOldQuantifiers(result, cSpec.getTerm2Old(),
0585: false, null);
0586: }
0587:
0588: if (!pm.isStatic()) {
0589: result = updatePrefix(result);
0590: }
0591:
0592: result = UsefulTools.addRepresents(result, services,
0593: (ProgramVariable) cSpec.getInstancePrefix());
0594: /* if(UsefulTools.purityCheck(result,
0595: services.getImplementation2SpecMap())
0596: != null){
0597: throw new RuntimeException("Nonpure method "+
0598: UsefulTools.purityCheck(result,
0599: services.getImplementation2SpecMap())+
0600: " used in the "+
0601: "specification for method "+
0602: pm.getName());
0603: }*/
0604: if (!pm.isStatic()) {
0605: result = UsefulTools.quantifySelf(result, pm
0606: .getMethodDeclaration(),
0607: (ProgramVariable) getPrefix());
0608: }
0609: result = bindSpecVars(result);
0610: return imp(func(services.getJavaInfo().getInReachableState()),
0611: UsefulTools.quantifyProgramVariables(result, params
0612: .allElements().iterator(), Op.ALL, services));
0613: }
0614:
0615: public Term bindSpecVars(Term t) {
0616: IteratorOfNamed it = specVars.iterator();
0617: while (it.hasNext()) {
0618: LogicVariable lv = (LogicVariable) it.next();
0619: t = tf.createQuantifierTerm(Op.ALL, lv, t);
0620: }
0621: return t;
0622: }
0623:
0624: public void addPre(Term t) {
0625: if (t != null) {
0626: pre = and(pre, t);
0627: }
0628: }
0629:
0630: public void addPost(Term t) {
0631: if (t != null) {
0632: post = and(post, t);
0633: }
0634: }
0635:
0636: public void setSpecVars(ListOfNamed svs) {
0637: specVars = svs;
0638: }
0639:
0640: public ListOfNamed getSpecVars() {
0641: return specVars;
0642: }
0643:
0644: public void addDiverges(Term t) {
0645: if (t != null) {
0646: diverges = or(diverges, t);
0647: }
0648: }
0649:
0650: private Term createdOrNull(ProgramVariable var) {
0651: final Term tVar = var(var);
0652: return or(equals(tVar, NULL(services)), UsefulTools.isCreated(
0653: tVar, services));
0654: }
0655:
0656: protected Term createModalityTermForEnsures(Term post,
0657: boolean desugar, boolean withInv, boolean allInv) {
0658: ModTermKey key = new ModTermKey(post, desugar, withInv, allInv);
0659: Term c = (Term) modalityTermForEnsuresCache.get(key);
0660: if (c != null) {
0661: return c;
0662: }
0663: Term excPost = tt();
0664: Term excVarTerm = var(excVar);
0665: post = imp(equals(excVarTerm, nullTerm), post);
0666: final IteratorOfSignals it = signals.iterator();
0667: while (it.hasNext()) {
0668: final Signals sig = it.next();
0669: final SortDefiningSymbols s = (SortDefiningSymbols) (sig
0670: .type().getSort());
0671: final InstanceofSymbol func = (InstanceofSymbol) s
0672: .lookupSymbol(InstanceofSymbol.NAME);
0673:
0674: Term post1 = imp(equals(func(func, excVarTerm), BOOL_TRUE),
0675: sig.condition());
0676:
0677: if (sig.variable() != null) {
0678: post1 = tf.createUpdateTerm(var(sig.variable()),
0679: excVarTerm, post1);
0680: }
0681: excPost = and(excPost, post1);
0682: }
0683:
0684: final JavaBlock jb = catchAllJB(desugar);
0685: if (excPost != null) {
0686: excPost = imp(not(equals(excVarTerm, nullTerm)), excPost);
0687: post = and(post, excPost);
0688: }
0689: if (withInv
0690: && !services.getImplementation2SpecMap().getModifiers(
0691: pm).contains("helper")) {
0692: post = cSpec.addClassSpec2Post(post, true, !allInv, pm,
0693: cSpec);
0694: if (allInv) {
0695: Term ai = UsefulTools.allInvariants(services
0696: .getImplementation2SpecMap());
0697: if (ai != null) {
0698: post = and(ai, post);
0699: }
0700: }
0701: }
0702: post = updatePrefix(post);
0703: post = UsefulTools.addRepresents(post, services,
0704: (ProgramVariable) cSpec.getInstancePrefix());
0705: if (diverges == null || ff().equals(diverges)) {
0706: c = dia(jb, post);
0707: } else {
0708: c = box(jb, post);
0709: }
0710: modalityTermForEnsuresCache.put(key, c);
0711: return c;
0712: }
0713:
0714: /**
0715: * creates and sets the self (this) prefix variable. In addition implicit
0716: * method preconditions are added. Implicit means the JML semantics requires them to
0717: * be fulfilled and therefore the specifier does not need to state them explicitly.
0718: * Such invariants are, e.g.
0719: * <ul>
0720: * <li> "this" (self) is not null and it is a created object</li>
0721: * </ul>
0722: */
0723: private void createSelfAndAddImplicitPreconditions(
0724: ProgramMethod pm, Services services, JMLClassSpec cSpec) {
0725: self = (ProgramVariable) cSpec.getInstancePrefix();
0726: Term t_self = var(self);
0727: //adds self!=null && self.<created> == true or
0728: //self.<classInitialized> == true to the precondition
0729: if (!(pm.getMethodDeclaration() instanceof Constructor)) {
0730: addPre(not(equals(t_self, nullTerm)));
0731: addPre(UsefulTools.isCreated(t_self, services));
0732: }
0733: }
0734:
0735: /**
0736: * add implicit preconditions for static methods, like:
0737: * class is initialized etc.
0738: */
0739: private void addImplicitPreconditionsForStaticMethods(
0740: Services services) {
0741: final ProgramVariable ci = ji.getAttribute(
0742: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED, services
0743: .getJavaInfo().getKeYJavaType(cd));
0744: addPre(equals(var(ci), BOOL_TRUE));
0745: }
0746:
0747: public boolean containsQuantifiedAssignableLocation() {
0748: IteratorOfLocationDescriptor it = assignableVariables
0749: .iterator();
0750: while (it.hasNext()) {
0751: LocationDescriptor loc = it.next();
0752: if (containsQuantifiedLocationHelp(loc)) {
0753: return true;
0754: }
0755: }
0756: return false;
0757: }
0758:
0759: private boolean containsQuantifiedLocationHelp(
0760: LocationDescriptor loc) {
0761: if (loc instanceof BasicLocationDescriptor) {
0762: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
0763: return !bloc.getFormula().equals(tt())
0764: || bloc.getLocTerm().freeVars().size() > 0;
0765: }
0766: return false;
0767: }
0768:
0769: public String getAssignableMode() {
0770: if (services.getImplementation2SpecMap().getModifiers(pm)
0771: .contains("pure")
0772: && assignableVariables == SetAsListOfLocationDescriptor.EMPTY_SET) {
0773: return "nothing";
0774: }
0775: if (assignableVariables == SetAsListOfLocationDescriptor.EMPTY_SET
0776: && assignableMode == null) {
0777: return EVERYTHING;
0778: }
0779: // an inconsistent case
0780: if (assignableVariables != SetAsListOfLocationDescriptor.EMPTY_SET
0781: && "nothing".equals(assignableMode)) {
0782: return null;
0783: }
0784: return assignableMode;
0785: }
0786:
0787: public CatchAllStatement getCatchAllStatement() {
0788: return catchAllStmt;
0789: }
0790:
0791: public TypeDeclaration getClassDeclaration() {
0792: return cd;
0793: }
0794:
0795: public Term getCompletePost(boolean withClassSpec, boolean allInv) {
0796: Term result;
0797: if (oldLVs == null) {
0798: getPi1();
0799: }
0800: if (getPost() == null) {
0801: result = createModalityTermForEnsures(tt(), false,
0802: withClassSpec, allInv);
0803: } else {
0804: result = createModalityTermForEnsures(getPost(), false,
0805: withClassSpec, allInv);
0806: }
0807: result = result.sub(0);
0808: result = addOldQuantifiers(result, lv2old, false, params);
0809: if (!(pm.getMethodDeclaration() instanceof Constructor)) {
0810: result = updatePrefix(result);
0811: }
0812: if (resultVar != null && resultVar.sort() instanceof ObjectSort) {
0813: result = and(result, createdOrNull(resultVar));
0814: }
0815: return result;
0816: }
0817:
0818: public Term getCompletePostFunctional(boolean withClassSpec,
0819: boolean allInv) {
0820: Term t = getCompletePost(withClassSpec, allInv);
0821: return replaceFreeVarsWithConsts(t);
0822: }
0823:
0824: /**
0825: * returns the precondition + represents for model fields
0826: * (+ invariants iff withClassSpec = true, + the negation of the diverges
0827: * clause in order to retrieve a precondition under which the method must
0828: * terminate).
0829: */
0830: public Term getCompletePre(boolean withClassSpec, boolean allInv,
0831: boolean terminationCase) {
0832: Term t = getPre();
0833: if (withClassSpec) {
0834: if (allInv
0835: && !services.getImplementation2SpecMap()
0836: .getModifiers(pm).contains("helper")) {
0837: Term ai = UsefulTools.allInvariants(services
0838: .getImplementation2SpecMap());
0839: t = UsefulTools.makeConjunction(t, ai);
0840: } else {
0841: t = cSpec.addClassSpec2Pre(t, pm, cSpec);
0842: }
0843: }
0844: if (terminationCase && diverges != null
0845: && !ff().equals(diverges)) {
0846: Term divPre = not(diverges);
0847: divPre = updatePrefix(divPre);
0848: t = and(divPre, t);
0849: }
0850: t = UsefulTools.addRepresents(t, services,
0851: (ProgramVariable) cSpec.getInstancePrefix());
0852: t = updatePrefix(t);
0853: return t == null ? tt() : t;
0854: }
0855:
0856: /**
0857: * returns the ProgramVariable that is used for expressing the excetional
0858: * behavior of a method.
0859: */
0860: public ProgramVariable getExceptionVariable() {
0861: return excVar;
0862: }
0863:
0864: public ReferencePrefix getInheritedPrefix() {
0865: return inheritedPrefix;
0866: }
0867:
0868: public String getJavaPath() {
0869: return javaPath;
0870: }
0871:
0872: public MethodDeclaration getMethodDeclaration() {
0873: return pm.getMethodDeclaration();
0874: }
0875:
0876: public JavaModelMethod getModelMethod() {
0877: return new JavaModelMethod(getProgramMethod(), javaPath,
0878: services);
0879: }
0880:
0881: public NamespaceSet getNamespaces() {
0882: return nss;
0883: }
0884:
0885: public ProgramVariable getParameterAt(int i) {
0886: return (ProgramVariable) pm.getParameters()
0887: .getParameterDeclaration(i).getVariableSpecification()
0888: .getProgramVariable();
0889: }
0890:
0891: public ListOfQuantifierPrefixEntry getOldLVs() {
0892: if (oldLVs == null) {
0893: getPi1();
0894: }
0895: return oldLVs;
0896: }
0897:
0898: public ListOfOperator getOldFuncSymbols() {
0899: if (oldFuncSymbols == null) {
0900: getPi1();
0901: }
0902: return oldFuncSymbols;
0903: }
0904:
0905: public Term getPi1() {
0906: if (pi1 == null) {
0907: lv2old = new TreeMap(comparator);
0908: LinkedList l = new LinkedList();
0909: LinkedList oldFS = new LinkedList();
0910: pi1 = getPi1Helper(tt(), l, oldFS, term2old);
0911: pi1 = getPi1Helper(pi1, l, oldFS, cSpec.getTerm2Old());
0912: pi1 = UsefulTools.addRepresents(pi1, services,
0913: (ProgramVariable) cSpec.getInstancePrefix());
0914: oldLVs = QuantifierPrefixEntry
0915: .toUniversalList(l.iterator());
0916: oldFuncSymbols = toOpList(oldFS);
0917: }
0918: return pi1;
0919: }
0920:
0921: private ListOfOperator toOpList(List l) {
0922: ListOfOperator result = SLListOfOperator.EMPTY_LIST;
0923: Iterator it = l.iterator();
0924: while (it.hasNext()) {
0925: result = result.append((Operator) it.next());
0926: }
0927: return result;
0928: }
0929:
0930: public Term getPi1Functional() {
0931: return replaceFreeVarsWithConsts(getPi1());
0932: }
0933:
0934: private Term getPi1Helper(Term pi1, LinkedList l, LinkedList oldFS,
0935: HashMap map) {
0936: Set sortedKeyset = new TreeSet(comparator);
0937: sortedKeyset.addAll(map.keySet());
0938: final Iterator it = sortedKeyset.iterator();
0939: Term postAndInvTerm = createModalityTermForEnsures(
0940: getPost() == null ? tt() : getPost(), false, true,
0941: false);
0942: while (it.hasNext()) {
0943: Term t = (Term) it.next();
0944: Term old = (Term) map.get(t);
0945: if (UsefulTools.occursIn(old, postAndInvTerm, false)) {
0946: Term t1 = createEqualityTermForOldLV(t, old, l, oldFS,
0947: lv2old);
0948: if (pi1 == tt()) {
0949: pi1 = t1;
0950: } else {
0951: pi1 = and(pi1, t1);
0952: }
0953: }
0954: }
0955: return pi1;
0956: }
0957:
0958: /**
0959: * returns the locally declared postcondition
0960: */
0961: public Term getPost() {
0962: return post;
0963: }
0964:
0965: /**
0966: * returns the locally declared precondition
0967: */
0968: public Term getPre() {
0969: return pre;
0970: }
0971:
0972: public ReferencePrefix getPrefix() {
0973: if (pm != null && pm.isStatic()) {
0974: return cSpec.getStaticPrefix();
0975: } else {
0976: return cSpec.getInstancePrefix();
0977: }
0978: }
0979:
0980: public ProgramMethod getProgramMethod() {
0981: return pm;
0982: }
0983:
0984: public ProgramElement getProofStatement() {
0985: return createModalityTermForEnsures(post == null ? tt() : post,
0986: false, false, false).javaBlock().program();
0987: }
0988:
0989: public ProgramVariable getResultVar() {
0990: if (resultVar == null) {
0991: resultVar = makeResultVar();
0992: }
0993: return resultVar;
0994: }
0995:
0996: public ProgramVariable getSelf() {
0997: return self;
0998: }
0999:
1000: public Services getServices() {
1001: return services;
1002: }
1003:
1004: public SetOfSignals getSignals() {
1005: return signals;
1006: }
1007:
1008: public LinkedHashMap getTerm2Old() {
1009: return term2old;
1010: }
1011:
1012: public int id() {
1013: return id;
1014: }
1015:
1016: /**
1017: * Checks if name, signature, accessibility and so on are equal for
1018: * this.pm and pm. If this.pm and pm occur on the same branch in the
1019: * class hierarchy must be checked somewhere else!
1020: */
1021: public boolean isCloneableFor(ProgramMethod method) {
1022: if (!method.getName().equals(this .pm.getName())) {
1023: return false;
1024: }
1025:
1026: final TypeReference methTypeRef = method.getTypeReference();
1027: if ((methTypeRef != null && !methTypeRef.equals(this .pm
1028: .getTypeReference()))
1029: || (methTypeRef == null && this .pm.getTypeReference() != null)) {
1030: return false;
1031: }
1032:
1033: final Throws methThrown = method.getThrown();
1034: if ((methThrown != null && !methThrown.equals(this .pm
1035: .getThrown()))
1036: || (methThrown == null && this .pm.getThrown() != null)) {
1037: return false;
1038: }
1039:
1040: if (method.getParameterDeclarationCount() != this .pm
1041: .getParameterDeclarationCount()) {
1042: return false;
1043: }
1044: for (int i = 0; i < method.getParameterDeclarationCount(); i++) {
1045: if (!method.getParameterType(i).equals(
1046: this .pm.getParameterType(i))) {
1047: return false;
1048: }
1049: }
1050: final int methModSize = method.getModifiers().size();
1051: final int this PMethModSize = this .pm.getModifiers().size();
1052: if (methModSize != this PMethModSize
1053: + ((cd instanceof InterfaceDeclaration) ? 1 : 0)
1054: - (pm.isAbstract() ? 1 : 0)) {
1055: return false;
1056: }
1057:
1058: for (int i = 0; i < methModSize; i++) {
1059: boolean equal = false;
1060: final Modifier modifier = method.getModifiers()
1061: .getModifier(i);
1062:
1063: if (!((cd instanceof InterfaceDeclaration) && modifier instanceof Public)) {
1064:
1065: for (int j = 0; j < this PMethModSize; j++) {
1066: if (modifier.equals(this .pm.getModifiers()
1067: .getModifier(j))) {
1068: equal = true;
1069: break;
1070: }
1071: }
1072: if (!equal)
1073: return false;
1074: }
1075: }
1076: return true;
1077: }
1078:
1079: public StatementBlock makeMBS() {
1080: if (mBS == null) {
1081: ArrayOfParameterDeclaration aopd = pm.getParameters();
1082: Expression[] aop = new Expression[pm.getParameters().size()];
1083: for (int i = 0; i < aopd.size(); i++) {
1084: aop[i] = (ProgramVariable) aopd
1085: .getParameterDeclaration(i)
1086: .getVariableSpecification()
1087: .getProgramVariable();
1088: }
1089: if (!(pm.getMethodDeclaration() instanceof Constructor)) {
1090: MethodBodyStatement mb = new MethodBodyStatement(pm, pm
1091: .isStatic() ? null : getPrefix(),
1092: getResultVar(), new ArrayOfExpression(aop));
1093: mBS = new StatementBlock(mb);
1094: } else {
1095: New n = new New(aop, (TypeReference) cSpec
1096: .getStaticPrefix(), null);
1097: MethodFrame fakeFrame = new MethodFrame(null,
1098: new ExecutionContext((TypeReference) cSpec
1099: .getStaticPrefix(), null),
1100: new StatementBlock(new CopyAssignment(
1101: (ProgramVariable) getPrefix(), n)));
1102: mBS = new StatementBlock(fakeFrame);
1103: }
1104: }
1105: return mBS;
1106: }
1107:
1108: private ProgramVariable makeResultVar() {
1109: if (pm.getTypeReference() == null) {
1110: return null;
1111: }
1112: ProgramVariable v = new LocationVariable(
1113: new ProgramElementName("_jmlresult"
1114: + (resultVarCount++)), pm.getTypeReference()
1115: .getKeYJavaType());
1116: progVarNS.add(v);
1117: return v;
1118: }
1119:
1120: public Term replaceFreeVarsWithConsts(Term t) {
1121: SetOfQuantifiableVariable vars = t.freeVars();
1122: if (vars.size() == 0) {
1123: return t;
1124: }
1125: IteratorOfQuantifiableVariable it = vars.iterator();
1126: while (it.hasNext()) {
1127: QuantifiableVariable qv = it.next();
1128: if (lv2const == null) {
1129: lv2const = new TreeMap(comparator);
1130: }
1131: if (!lv2const.containsKey(qv)) {
1132: lv2const.put(qv, new RigidFunction(qv.name(),
1133: qv.sort(), new Sort[0]));
1134:
1135: }
1136: }
1137: Iterator entriesIt = lv2const.entrySet().iterator();
1138: while (entriesIt.hasNext()) {
1139: Map.Entry e = (Map.Entry) entriesIt.next();
1140: ClashFreeSubst subst = new ClashFreeSubst(
1141: (QuantifiableVariable) e.getKey(),
1142: func((RigidFunction) e.getValue()));
1143: t = subst.apply(t);
1144: }
1145: return t;
1146: }
1147:
1148: public Collection introducedConstants() {
1149: return new HashSet(getLv2Const().values());
1150: }
1151:
1152: public SetOfLocationDescriptor replaceModelFieldsInAssignable() {
1153: return replaceModelFieldsInAssignable(cSpec);
1154: }
1155:
1156: public SetOfLocationDescriptor replaceModelFieldsInAssignable(
1157: JMLClassSpec cs) {
1158: if (assignableVariables == SetAsListOfLocationDescriptor.EMPTY_SET) {
1159: if ("nothing".equals(getAssignableMode())) {
1160: return assignableVariables;
1161: } else {
1162: return null;
1163: }
1164: }
1165: SetOfLocationDescriptor result = assignableVariables;
1166: /* IteratorOfTerm it = assignableVariables.iterator();
1167: while(it.hasNext()){
1168: Term varTerm = it.next();
1169: System.out.println("replaceModelFieldsInAssignable3: "+varTerm);
1170: Term rep = (Term) cs.getRepresents().get(varTerm);
1171: System.out.println("replaceModelFieldsInAssignable4: "+rep);
1172: if(rep != null){
1173: System.out.println("replaceModelFieldsInAssignable5");
1174: result = result.remove(varTerm).add(rep);
1175: }
1176: }*/
1177: return result;
1178: }
1179:
1180: /**
1181: * Replaces occurences of the inherited prefix and the inherited parameters
1182: * in <code>t</code> with the current prefix and the current parameters,
1183: * respectively.
1184: */
1185: private Term replaceSelf(Term t) {
1186: if (t.op() == inheritedPrefix) {
1187: return var(self);
1188: } else if (t.op() instanceof ProgramVariable) {
1189: if (params.lookup(t.op().name()) != null) {
1190: return var((ProgramVariable) params.lookup(t.op()
1191: .name()));
1192: }
1193: return t;
1194: } else {
1195: Term[] subs = new Term[t.arity()];
1196: for (int i = 0; i < t.arity(); i++) {
1197: subs[i] = replaceSelf(t.sub(i));
1198: }
1199: return tf.createTerm(t.op(), subs,
1200: (ArrayOfQuantifiableVariable) null, null);
1201: }
1202: }
1203:
1204: public void setAssignableMode(String s) {
1205: assignableMode = s;
1206: }
1207:
1208: public void setId(int id) {
1209: this .id = id;
1210: }
1211:
1212: /**
1213: * returns true if this specification demands termination of the method,
1214: * which means in this case that terminating by throwing an exception
1215: * is also considered to be a termination.
1216: */
1217: public boolean terminates() {
1218: return diverges == null || diverges.equals(ff());
1219: }
1220:
1221: private void updateAssignableLocations() {
1222: if (!(pm.isStatic() || pm.getMethodDeclaration() instanceof Constructor)) {
1223: IteratorOfLocationDescriptor it = assignableVariables
1224: .iterator();
1225: assignableVariables = SetAsListOfLocationDescriptor.EMPTY_SET;
1226: while (it.hasNext()) {
1227: LocationDescriptor loc = it.next();
1228: LocationDescriptor newLoc;
1229: if (loc instanceof BasicLocationDescriptor) {
1230: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
1231: newLoc = new BasicLocationDescriptor(
1232: replaceSelf(bloc.getFormula()),
1233: replaceSelf(bloc.getLocTerm()));
1234:
1235: } else {
1236: Debug
1237: .assertTrue(loc instanceof EverythingLocationDescriptor);
1238: newLoc = loc;
1239: }
1240: assignableVariables = assignableVariables.add(newLoc);
1241: }
1242: }
1243: }
1244:
1245: protected Term updateParameters(
1246: ArrayOfParameterDeclaration oldParams,
1247: ArrayOfParameterDeclaration newParams, Term target) {
1248: if (target == null)
1249: return null;
1250: for (int i = 0; i < newParams.size(); i++) {
1251: final ProgramVariable oldP = (ProgramVariable) oldParams
1252: .getParameterDeclaration(i)
1253: .getVariableSpecification().getProgramVariable();
1254: final ProgramVariable newP = (ProgramVariable) newParams
1255: .getParameterDeclaration(i)
1256: .getVariableSpecification().getProgramVariable();
1257: target = tf.createUpdateTerm(var(oldP), var(newP), target);
1258: }
1259: return simplifier.simplify(target, services);
1260: }
1261:
1262: protected Term updatePrefix(Term t) {
1263: if (!pm.isStatic() && t != null && inheritedPrefix != null) {
1264: t = tf.createUpdateTerm(
1265: var((ProgramVariable) inheritedPrefix), var(self),
1266: t);
1267: t = simplifier.simplify(t, services);
1268: }
1269: return t;
1270: }
1271:
1272: }
|