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:
017: package de.uka.ilkd.key.jml;
018:
019: import java.util.HashMap;
020: import java.util.LinkedHashMap;
021:
022: import de.uka.ilkd.key.java.*;
023: import de.uka.ilkd.key.java.abstraction.Constructor;
024: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
027: import de.uka.ilkd.key.java.declaration.*;
028: import de.uka.ilkd.key.java.declaration.modifier.Model;
029: import de.uka.ilkd.key.java.declaration.modifier.Public;
030: import de.uka.ilkd.key.java.declaration.modifier.Static;
031: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
032: import de.uka.ilkd.key.java.expression.operator.New;
033: import de.uka.ilkd.key.java.recoderext.ClassInitializeMethodBuilder;
034: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
035: import de.uka.ilkd.key.java.reference.ExecutionContext;
036: import de.uka.ilkd.key.java.reference.ReferencePrefix;
037: import de.uka.ilkd.key.java.reference.TypeRef;
038: import de.uka.ilkd.key.java.statement.*;
039: import de.uka.ilkd.key.logic.*;
040: import de.uka.ilkd.key.logic.op.*;
041: import de.uka.ilkd.key.logic.sort.Sort;
042: import de.uka.ilkd.key.util.ExtList;
043:
044: /** wraps specifications that are valid for the entire class (e.g. invariants
045: * or history constraints) or interface
046: */
047: public class JMLClassSpec extends JMLSpec {
048:
049: private Term instInv, instCon, staticInv, staticCon;
050: private LinkedHashMap term2old;
051: private LinkedHashMap represents;
052: // private HashMap suchthat;
053: private ReferencePrefix staticPrefix;
054: private ReferencePrefix instancePrefix;
055: private Services services;
056: /** the class or interfacedeclaration this specification refers to */
057: private TypeDeclaration cd;
058: // the KeYJavaType of cd
059: private KeYJavaType type;
060: private Namespace modelVars;
061: private Namespace modelMethods;
062: private NamespaceSet nss;
063: private KeYJavaType objectKeYJavaType;
064: protected static Term trueTerm = null;
065: protected static Term falseTerm = null;
066: private String javaPath;
067:
068: // flag which is set to false iff static initialisation features should be suppressed
069: protected boolean staticInit = false;
070:
071: public JMLClassSpec(Services services, TypeDeclaration cd,
072: NamespaceSet nss, String javaPath) {
073:
074: progVarNS = new Namespace();
075: funcNS = new Namespace();
076:
077: term2old = new LinkedHashMap();
078: this .services = services;
079: objectKeYJavaType = services.getJavaInfo().getJavaLangObject();
080:
081: this .cd = cd;
082: instCon = null;
083: staticCon = null;
084: instInv = null;
085: staticInv = null;
086:
087: type = services.getJavaInfo().getKeYJavaType(cd);
088: staticPrefix = new TypeRef(type);
089: instancePrefix = new LocationVariable(new ProgramElementName(
090: "self_"
091: + cd.getName().replace('.', '_').replace('<',
092: '_').replace('>', '_')), type);
093: progVarNS.add((ProgramVariable) instancePrefix);
094: modelVars = new Namespace();
095: modelMethods = new Namespace();
096: represents = new LinkedHashMap();
097: // suchthat = new HashMap();
098: this .nss = nss;
099: services.getImplementation2SpecMap().addClassSpec(this );
100: if (trueTerm == null) {
101: trueTerm = tt();
102: }
103: if (falseTerm == null) {
104: falseTerm = ff();
105: }
106: this .javaPath = javaPath;
107: }
108:
109: public boolean containsInvOrConst() {
110: return (staticCon != null || staticInv != null
111: || instCon != null || instInv != null);
112: }
113:
114: public Services getServices() {
115: return services;
116: }
117:
118: /**
119: * returns the class or interfacedeclaration this specification refers to.
120: */
121: public TypeDeclaration getClassDeclaration() {
122: return cd;
123: }
124:
125: public ReferencePrefix getInstancePrefix() {
126: return instancePrefix;
127: }
128:
129: public ReferencePrefix getStaticPrefix() {
130: return staticPrefix;
131: }
132:
133: public void addInstanceInvariant(Term t) {
134: instInv = UsefulTools.makeConjunction(instInv, t);
135: }
136:
137: public void addStaticInvariant(Term t) {
138: staticInv = UsefulTools.makeConjunction(staticInv, t);
139: }
140:
141: public void addInstanceConstraint(Term t) {
142: instCon = UsefulTools.makeConjunction(instCon, t);
143: }
144:
145: public void addStaticConstraint(Term t) {
146: staticCon = UsefulTools.makeConjunction(staticCon, t);
147: }
148:
149: public void addModelVariable(ProgramVariable v) {
150: // nss.programVariables().add(v);
151: modelVars.add(v);
152: if (cd instanceof InterfaceDeclaration) {
153: addRepresents(v, null);
154: }
155: }
156:
157: public void addModelMethod(ProgramMethod pm) {
158: modelMethods.add(pm);
159: }
160:
161: /**
162: * returns the model variables declared in this class
163: */
164: public Namespace getModelVars() {
165: return modelVars;
166: }
167:
168: /**
169: * returns the model methods declared in this class
170: */
171: public Namespace getModelMethods() {
172: return modelMethods;
173: }
174:
175: /**
176: * adds the representation <code>rep</code> for the model variable
177: * <code>var</code>.
178: */
179: public void addRepresents(Term loc, Term rep) {
180: addRepresents(getPV((Location) loc.op()), rep);
181: }
182:
183: /**
184: * adds the representation <code>rep</code> for the model variable
185: * <code>var</code>.
186: */
187: public void addRepresents(ProgramVariable v, Term rep) {
188: ProgramMethod pm = createProgramMethodForMV(v);
189: modelMethods.add(pm);
190: if (rep != null) {
191: JMLMethodSpec spec = new JMLNormalMethodSpec(pm, services,
192: new Namespace(), new LinkedHashMap(), this , nss,
193: javaPath);
194: spec.setAssignableMode("nothing");
195: if (rep.sort() == Sort.FORMULA) {
196: if ((rep.op() instanceof Equality)
197: && rep.sub(1) != null
198: && rep.sub(1).equals(JMLMethodSpec.BOOL_TRUE)) {
199: spec.addPost(equals(var(spec.getResultVar()), rep
200: .sub(0)));
201: } else if (rep.op() == Op.TRUE) {
202: spec.addPost(equals(var(spec.getResultVar()),
203: JMLMethodSpec.BOOL_TRUE));
204: } else {
205: Term eq = equals(var(spec.getResultVar()),
206: JMLMethodSpec.BOOL_TRUE);
207: spec.addPost(equiv(eq, rep));
208: }
209: } else {
210: spec.addPost(equals(var(spec.getResultVar()), rep));
211: }
212: }
213: represents.put(v, getTermForModelMethod(pm));
214: }
215:
216: /**
217: * the loc is either a programvariable or an attribute
218: * in the first case loc itself in the latter one loc.attribute()
219: * is returned
220: */
221: private ProgramVariable getPV(Location loc) {
222: if (loc instanceof ProgramVariable) {
223: return (ProgramVariable) loc;
224: }
225: return (ProgramVariable) ((AttributeOp) loc).attribute();
226: }
227:
228: public void addSuchThat(Term t_loc, Term axiom) {
229: ProgramVariable v = getPV((Location) t_loc.op());
230: ProgramMethod pm = createProgramMethodForMV(v);
231:
232: represents.put(v, getTermForModelMethod(pm));
233: modelMethods.add(pm);
234: JMLMethodSpec spec = new JMLNormalMethodSpec(pm, services,
235: new Namespace(), new LinkedHashMap(), this , nss,
236: javaPath);
237: spec.setAssignableMode("nothing");
238: spec.addPost(tf.createUpdateTerm(t_loc,
239: var(spec.getResultVar()), axiom));
240: spec.addPre(getExTermForModelVar(t_loc, axiom));
241: }
242:
243: /**
244: * returns a mapping from modelmethods to their specifications.
245: */
246: public HashMap buildModelMethod2Specs() {
247: HashMap modelMethod2Specs = new HashMap();
248: IteratorOfNamed it = modelMethods.allElements().iterator();
249: Implementation2SpecMap ism = services
250: .getImplementation2SpecMap();
251: while (it.hasNext()) {
252: ProgramMethod pm = (ProgramMethod) it.next();
253: modelMethod2Specs.put(pm, ism.getSpecsForMethod(pm));
254: }
255: return modelMethod2Specs;
256: }
257:
258: /**
259: * returns a HashMap that contains the locally defined and inherited
260: * represents relations.
261: */
262: public HashMap getRepresents() {
263: HashMap result = new HashMap();
264: KeYJavaType kjt = services.getJavaInfo().getSuperclass(type);
265: if (kjt == null) {
266: kjt = objectKeYJavaType;
267: }
268: JMLClassSpec super Spec = services.getImplementation2SpecMap()
269: .getSpecForClass(kjt);
270: if (super Spec != null && (cd instanceof ClassDeclaration)
271: && type != objectKeYJavaType) {
272: result.putAll(super Spec.getRepresents());
273: }
274: result.putAll(represents);
275: return result;
276: }
277:
278: public LinkedHashMap getTerm2Old() {
279: return term2old;
280: }
281:
282: public Term getLocalInstanceInvariants() {
283: return instInv;
284: }
285:
286: public SetOfTerm getAllQuantifiedInvariants() {
287: return getQuantifiedInstanceInvariants().add(staticInv);
288: }
289:
290: public SetOfTerm getQuantifiedInstanceInvariants() {
291: Term result = null;
292: Term self = tf
293: .createVariableTerm((ProgramVariable) instancePrefix);
294: if (getInstanceInvariants() != null
295: && !trueTerm.equals(getInstanceInvariants())) {
296: Term eqn = not(equals(self, NULL(services)));
297: ProgramVariable created = services.getJavaInfo()
298: .getAttribute(ImplicitFieldAdder.IMPLICIT_CREATED,
299: objectKeYJavaType);
300: Term eqc = equals(dot(self, created),
301: JMLMethodSpec.BOOL_TRUE);
302: result = imp(and(eqn, eqc), getInstanceInvariants());
303: result = UsefulTools.addRepresents(result, services,
304: (ProgramVariable) instancePrefix);
305: LogicVariable selfLv = new LogicVariable(new Name("self_"
306: + cd.getName() + "_lv"), self.sort());
307: result = tf.createUpdateTerm(self, var(selfLv), result);
308: result = all(selfLv, result);
309: }
310: if (result == null) {
311: return SetAsListOfTerm.EMPTY_SET;
312: }
313: result = UsefulTools.addRepresents(result, services,
314: (ProgramVariable) instancePrefix);
315: return SetAsListOfTerm.EMPTY_SET.add(result);
316: }
317:
318: /**
319: * returns locally declared and inherited instance invariants.
320: */
321: public Term getInstanceInvariants() {
322: Term result = UsefulTools.makeConjunction(null, instInv);
323: Implementation2SpecMap ism = services
324: .getImplementation2SpecMap();
325: ListOfKeYJavaType l = cd.getSupertypes();
326: IteratorOfKeYJavaType it = l.iterator();
327: while (it.hasNext()) {
328: JMLClassSpec cs = ism.getSpecForClass(it.next());
329: if (cs != null) {
330: Term ii = cs.getInstanceInvariants();
331: if (ii != null) {
332: Term upd = tf.createUpdateTerm(
333: var((ProgramVariable) cs
334: .getInstancePrefix()),
335: var((ProgramVariable) getInstancePrefix()),
336: ii);
337: result = UsefulTools.makeConjunction(result, upd);
338: progVarNS.add(cs.getProgramVariableNS()
339: .allElements());
340: }
341: }
342: }
343: return result;
344: }
345:
346: public Term getLocalStaticInvariants() {
347: return staticInv;
348: }
349:
350: public Term getStaticInvariants() {
351: Term result = staticInv;
352: Implementation2SpecMap ism = services
353: .getImplementation2SpecMap();
354: ListOfKeYJavaType l = cd.getSupertypes();
355: IteratorOfKeYJavaType it = l.iterator();
356: while (it.hasNext()) {
357: JMLClassSpec cs = ism.getSpecForClass(it.next());
358: if (cs != null) {
359: result = UsefulTools.makeConjunction(result, cs
360: .getStaticInvariants());
361: progVarNS.add(cs.getProgramVariableNS().allElements());
362: }
363: }
364: return result;
365: }
366:
367: public Term getLocalInstanceConstraints() {
368: return instCon;
369: }
370:
371: public Term getInstanceConstraints() {
372: Term result = instCon;
373: Implementation2SpecMap ism = services
374: .getImplementation2SpecMap();
375: ListOfKeYJavaType l = cd.getSupertypes();
376: IteratorOfKeYJavaType it = l.iterator();
377: while (it.hasNext()) {
378: JMLClassSpec cs = ism.getSpecForClass(it.next());
379: if (cs != null) {
380: Term ic = cs.getInstanceConstraints();
381: if (ic != null) {
382: Term upd = tf.createUpdateTerm(
383: var((ProgramVariable) cs
384: .getInstancePrefix()),
385: var((ProgramVariable) getInstancePrefix()),
386: ic);
387: result = UsefulTools.makeConjunction(result, upd);
388: progVarNS.add(cs.getProgramVariableNS()
389: .allElements());
390: }
391: }
392: }
393: return result;
394: }
395:
396: public Term getLocalStaticConstraints() {
397: return staticCon;
398: }
399:
400: public Term getStaticConstraints() {
401: Term result = staticCon;
402: Implementation2SpecMap ism = services
403: .getImplementation2SpecMap();
404: ListOfKeYJavaType l = cd.getSupertypes();
405: IteratorOfKeYJavaType it = l.iterator();
406: while (it.hasNext()) {
407: JMLClassSpec cs = ism.getSpecForClass(it.next());
408: if (cs != null) {
409: result = UsefulTools.makeConjunction(result, cs
410: .getStaticConstraints());
411: progVarNS.add(cs.getProgramVariableNS().allElements());
412: }
413: }
414: return result;
415: }
416:
417: /** generates \exists x . p(x) where p is the relation for
418: * <code>modelvar</code> described by its represents-such_that clause.
419: */
420: public Term getExTermForModelVar(Term modelVar, Term axiom) {
421: LogicVariable lv = new LogicVariable(new Name(modelVar
422: .toString()
423: + "_jml_lv"), modelVar.sort());
424: Term result = tf.createUpdateTerm(modelVar, var(lv), axiom);
425: return ex(lv, result);
426: }
427:
428: public ProgramVariable lookupModelField(Name name)
429: throws AmbigiousModelElementException {
430: if (modelVars.lookup(name) != null) {
431: return (ProgramVariable) modelVars.lookup(name);
432: }
433: Implementation2SpecMap ism = services
434: .getImplementation2SpecMap();
435: ListOfKeYJavaType st = cd.getSupertypes();
436: boolean hasNonInterfaceST = false;
437: IteratorOfKeYJavaType it = st.iterator();
438: ProgramVariable result = null;
439: while (it.hasNext()) {
440: KeYJavaType kjt = it.next();
441: if ((kjt.getJavaType() instanceof ClassDeclaration)) {
442: hasNonInterfaceST = true;
443: }
444: JMLClassSpec cs = ism.getSpecForClass(kjt);
445: if (cs != null) {
446: ProgramVariable p = cs.lookupModelField(name);
447: if (p != null) {
448: if (result == null) {
449: result = p;
450: } else {
451: // throw new AmbigiousModelElementException(result);
452: }
453: }
454: }
455: }
456: if (result == null && type != objectKeYJavaType
457: && !hasNonInterfaceST) {
458: if (ism.getSpecForClass(objectKeYJavaType) == null) {
459: return result;
460: }
461: result = ism.getSpecForClass(objectKeYJavaType)
462: .lookupModelField(name);
463: }
464: return result;
465: }
466:
467: /**
468: * Returns the Term ((self!=null & self.created=true) -> instanceInvariants
469: * ) & staticInvariants, which is sometimes needed in POs.
470: */
471: public Term getAllLocalInvariants() {
472: Term result = null;
473: Term self = var((ProgramVariable) instancePrefix);
474: if (getLocalInstanceInvariants() != null
475: && !trueTerm.equals(getLocalInstanceInvariants())) {
476: final Term eqn = not(equals(self, NULL(services)));
477: final Term eqc = UsefulTools.isCreated(self, services);
478:
479: result = imp(and(eqn, eqc), getLocalInstanceInvariants());
480:
481: result = UsefulTools.addRepresents(result, services,
482: (ProgramVariable) instancePrefix);
483: LogicVariable selfLv = new LogicVariable(new Name("self_"
484: + cd.getName() + "_lv"), self.sort());
485: result = tf.createUpdateTerm(self, var(selfLv), result);
486: result = all(selfLv, result);
487: }
488: if (getLocalStaticInvariants() != null
489: && !trueTerm.equals(getLocalStaticInvariants())) {
490: Term si;
491: if (staticInit) {
492: ProgramVariable ci = services
493: .getJavaInfo()
494: .getAttribute(
495: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
496: type);
497: si = equals(var(ci), JMLMethodSpec.BOOL_TRUE);
498: si = imp(si, getLocalStaticInvariants());
499: } else {
500: si = getLocalStaticInvariants();
501: }
502: si = UsefulTools.addRepresents(si, services,
503: (ProgramVariable) instancePrefix);
504: result = UsefulTools.makeConjunction(result, si);
505: }
506: if (result == null) {
507: return null;
508: }
509: result = UsefulTools.addRepresents(result, services,
510: (ProgramVariable) instancePrefix);
511: return result;
512: }
513:
514: /**
515: * returns the model method with the name <code>name</code>,
516: * iff it is loacally declared within the type that is specified by this
517: * specification.
518: */
519: public ProgramMethod lookupModelMethodLocally(String name) {
520: if (modelMethods.lookup(new Name(type.getSort().toString()
521: + "::" + name)) != null) {
522: return (ProgramMethod) modelMethods.lookup(new Name(type
523: .getSort().toString()
524: + "::" + name.toString()));
525: }
526: return null;
527: }
528:
529: public ProgramMethod lookupModelMethod(Name name)
530: throws AmbigiousModelElementException {
531: if (modelMethods.lookup(new Name(type.getSort().toString()
532: + "::" + name.toString())) != null) {
533: return (ProgramMethod) modelMethods.lookup(new Name(type
534: .getSort().toString()
535: + "::" + name.toString()));
536: }
537: Implementation2SpecMap ism = services
538: .getImplementation2SpecMap();
539: ListOfKeYJavaType st = cd.getSupertypes();
540: IteratorOfKeYJavaType it = st.iterator();
541: ProgramMethod result = null;
542: while (it.hasNext()) {
543: KeYJavaType kjt = it.next();
544: if (ism.getSpecForClass(kjt) != null
545: && ism.getSpecForClass(kjt).lookupModelMethod(name) != null) {
546: if (result == null) {
547: result = ism.getSpecForClass(kjt)
548: .lookupModelMethod(name);
549: } else {
550: throw new AmbigiousModelElementException(result);
551: }
552: }
553: }
554: return result;
555: }
556:
557: protected Term getTermForModelMethod(ProgramMethod pm) {
558: Term[] sub;
559: if (pm.isStatic()) {
560: sub = new Term[0];
561: } else {
562: sub = new Term[1];
563: sub[0] = var((ProgramVariable) instancePrefix);
564: }
565: return func(pm, sub);
566: }
567:
568: /**
569: * creates a ProgramMethod and the Term for substituting the
570: * corresponding Model Variable.
571: */
572: private ProgramMethod createProgramMethodForMV(ProgramVariable mv) {
573: ExtList l = new ExtList();
574: l.add(new ProgramElementName(mv.name().toString() + "_rep"));
575: if (mv.isStatic()) {
576: l.add(new Static());
577: }
578: l.add(new Model());
579: l.add(new Public());
580: l.add(new TypeRef(mv.getKeYJavaType()));
581: MethodDeclaration md = new MethodDeclaration(l, false);
582: ProgramMethod pm = new ProgramMethod(md, type, mv
583: .getKeYJavaType(), PositionInfo.UNDEFINED);
584: services.getImplementation2SpecMap().addModifier(pm, "pure");
585: services.getImplementation2SpecMap().addModifier(pm, "helper");
586: if (nss.functions().lookup(pm.name()) == null) {
587: nss.functions().add(pm);
588: }
589: return pm;
590: }
591:
592: /**
593: * returns a term of the form inv -> <{try{ m();}catch(Exception e)}>inv
594: * If <code>allInv</code> is true, inv is a conjunction of all
595: * (static and instance) invariants of every existing type or just
596: * the invariants of this type specification otherwise.
597: */
598: public Term getPreservesInvariantBehavior(ProgramMethod md,
599: boolean allInv) {
600: if (!services.getImplementation2SpecMap().getModifiers(md)
601: .contains("helper")
602: && (!md.isStatic()
603: && (getInstanceInvariants() != null || getInstanceConstraints() != null)
604: || getStaticInvariants() != null
605: || getStaticConstraints() != null || allInv)) {
606: Term excPre, excPost, result;
607: result = excPre = excPost = null;
608: KeYJavaType exc = services.getJavaInfo()
609: .getTypeByClassName("java.lang.Exception");
610: Branch[] catches = new Branch[1];
611: StatementBlock catchBody = new StatementBlock();
612: ProgramVariable e = new LocationVariable(
613: new ProgramElementName("_exc"
614: + (JMLMethodSpec.exceptionVarCount++)), exc);
615: progVarNS.add(e);
616: ParameterDeclaration param = new ParameterDeclaration(
617: new Modifier[0], new TypeRef(exc),
618: new VariableSpecification(e), false);
619: catches[0] = new Catch(param, catchBody);
620: excPost = addClassSpec2Post(excPost, true, !allInv, md,
621: this );
622: excPost = UsefulTools.addRepresents(excPost, services,
623: (ProgramVariable) instancePrefix);
624: if (allInv) {
625: Term ai = UsefulTools.allInvariants(services
626: .getImplementation2SpecMap());
627: excPre = UsefulTools.makeConjunction(ai, excPre);
628: excPost = UsefulTools.makeConjunction(ai, excPost);
629: } else {
630: excPre = addClassSpec2Pre(excPre, md, this );
631: }
632: StatementBlock tryBlock = new StatementBlock(new Try(
633: makeMBS(md.getMethodDeclaration()), catches));
634:
635: JavaBlock jb = JavaBlock.createJavaBlock(tryBlock);
636: if (excPost == null) {
637: return trueTerm;
638: }
639: excPost = box(jb, excPost);
640: if (excPre == null) {
641: result = excPost;
642: } else {
643: result = imp(excPre, excPost);
644: }
645: result = JMLMethodSpec.addOldQuantifiers(result,
646: getTerm2Old(), false, null);
647: result = UsefulTools.addRepresents(result, services,
648: (ProgramVariable) instancePrefix);
649: /* if(UsefulTools.purityCheck(result,
650: services.getImplementation2SpecMap())
651: != null){
652: throw new RuntimeException("Nonpure method "+
653: UsefulTools.purityCheck(result,
654: services.
655: getImplementation2SpecMap())+
656: " used in the "+
657: "specification for class/interface "
658: + cd.getName());
659: }*/
660:
661: //disjoins the methods preconditions
662: SetOfJMLMethodSpec specs = services
663: .getImplementation2SpecMap().getSpecsForMethod(md);
664: if (specs != null) {
665: specs = specs.union(services
666: .getImplementation2SpecMap()
667: .getInheritedMethodSpecs(md, type));
668: }
669: if (specs != null) {
670: Term invPre = falseTerm;
671: IteratorOfJMLMethodSpec it = specs.iterator();
672: while (it.hasNext()) {
673: JMLMethodSpec ms = it.next();
674: if (!(ms instanceof JMLPuritySpec)) {
675: invPre = or(ms.getCompletePre(false, false,
676: false), invPre);
677: }
678: }
679: if (invPre != falseTerm) {
680: result = imp(invPre, result);
681: }
682: }
683: result = imp(
684: selfIsCreatedAndNotNull((ProgramVariable) getInstancePrefix()),
685: result);
686: result = UsefulTools.quantifySelf(result, md
687: .getMethodDeclaration(),
688: (ProgramVariable) getInstancePrefix());
689: result = UsefulTools.quantifyProgramVariables(result,
690: UsefulTools
691: .getParameters(md.getMethodDeclaration())
692: .iterator(), Op.ALL, services);
693: return imp(func(services.getJavaInfo()
694: .getInReachableState()), result);
695: } else {
696: return trueTerm;
697: }
698: }
699:
700: private Term selfIsCreatedAndNotNull(ProgramVariable self) {
701: final Term selfAsTerm = var(self);
702: return and(not(equals(selfAsTerm, NULL(services))), UsefulTools
703: .isCreated(selfAsTerm, services));
704:
705: }
706:
707: /** Adds the applicable invariants of cSpec to the precondition of md
708: * iff md isn't declared with the modifier helper. md must be a member
709: * method of cSpec.
710: */
711: public Term addClassSpec2Pre(Term pre, ProgramMethod md,
712: JMLClassSpec cSpec) {
713: Term result;
714: if (md
715: .getName()
716: .equals(
717: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER)) {
718:
719: final ProgramVariable classInit = services
720: .getJavaInfo()
721: .getAttribute(
722: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
723: type);
724:
725: result = equals(var(classInit), JMLMethodSpec.BOOL_FALSE);
726: if (pre != null) {
727: result = and(pre, result);
728: }
729:
730: final ProgramVariable classErroneous = services
731: .getJavaInfo()
732: .getAttribute(
733: ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS,
734: type);
735: result = and(result, equals(var(classErroneous),
736: JMLMethodSpec.BOOL_FALSE));
737:
738: final ProgramVariable classInitInProgress = services
739: .getJavaInfo()
740: .getAttribute(
741: ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS,
742: type);
743: return and(result, equals(var(classInitInProgress),
744: JMLMethodSpec.BOOL_FALSE));
745: } else {
746: result = pre;
747: }
748:
749: if (cSpec == null
750: || md.getName().startsWith("<")
751: || services.getImplementation2SpecMap()
752: .getModifiers(md).contains("helper")) {
753: return pre;
754: }
755:
756: result = UsefulTools.makeConjunction(result, cSpec
757: .getStaticInvariants());
758:
759: if (!md.isStatic()
760: && !(md.getMethodDeclaration() instanceof ConstructorDeclaration)) {
761: result = UsefulTools.makeConjunction(result, cSpec
762: .getInstanceInvariants());
763: }
764: // result = addAxioms2Pre(result, true, false);
765: return result;
766: }
767:
768: /** Adds invariants and history constraints to the postcondition iff md
769: * isn't declared with the modifier helper.
770: */
771: public Term addClassSpec2Post(Term post, boolean constraints,
772: boolean invariants, ProgramMethod md, JMLClassSpec cSpec) {
773: if (cSpec == null
774: || services.getImplementation2SpecMap()
775: .getModifiers(md).contains("helper")) {
776: return post;
777: }
778: Term result = post == null ? tt() : post;
779: if ((!md.getName().startsWith("<") || md
780: .getName()
781: .equals(
782: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER))
783: && invariants) {
784: result = UsefulTools.makeConjunction(result, cSpec
785: .getStaticInvariants());
786: }
787: if (constraints && !md.getName().startsWith("<")) {
788: result = UsefulTools.makeConjunction(result, cSpec
789: .getStaticConstraints());
790: }
791: if (!md.isStatic() && !md.getName().startsWith("<")) {
792: if (invariants) {
793: result = UsefulTools.makeConjunction(result, cSpec
794: .getInstanceInvariants());
795: }
796: if (constraints && !(md.isConstructor())) {
797: result = UsefulTools.makeConjunction(result, cSpec
798: .getInstanceConstraints());
799: }
800: }
801: return and(func(services.getJavaInfo().getInReachableState()),
802: result);
803: }
804:
805: private StatementBlock makeMBS(MethodDeclaration md) {
806: StatementBlock mBS;
807: ArrayOfParameterDeclaration params = md.getParameters();
808: Expression[] aop = new Expression[md.getParameters().size()];
809: ProgramVariable result = null;
810: for (int i = 0; i < params.size(); i++) {
811: aop[i] = (ProgramVariable) params
812: .getParameterDeclaration(i)
813: .getVariableSpecification().getProgramVariable();
814: }
815: if (!(md instanceof Constructor)) {
816: KeYJavaType returnType;
817: if (md.getTypeReference() == null) {
818: returnType = services.getJavaInfo().getKeYJavaType(
819: "void");
820: } else {
821: returnType = md.getTypeReference().getKeYJavaType();
822: result = new LocationVariable(
823: new ProgramElementName("_jmlresult"
824: + (JMLMethodSpec.resultVarCount++)),
825: returnType);
826: progVarNS.add(result);
827: }
828: ProgramMethod pm = new ProgramMethod(md, type, returnType,
829: PositionInfo.UNDEFINED);
830: MethodBodyStatement mb = new MethodBodyStatement(pm, pm
831: .isStatic() ? null : getInstancePrefix(), result,
832: new ArrayOfExpression(aop));
833: mBS = new StatementBlock(mb);
834: } else {
835: final TypeRef typeRef = new TypeRef(type);
836: New n = new New(aop, typeRef, null);
837: mBS = new StatementBlock(new CopyAssignment(
838: (ProgramVariable) getInstancePrefix(), n));
839: mBS = new StatementBlock(new MethodFrame(null,
840: new ExecutionContext(typeRef, null), mBS));
841: }
842: return mBS;
843: }
844:
845: public String toString() {
846: return "Class specification for class " + cd.getName();
847: }
848:
849: }
|