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.LinkedHashMap;
020:
021: import de.uka.ilkd.key.java.ProgramElement;
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.java.StatementBlock;
024: import de.uka.ilkd.key.logic.JavaBlock;
025: import de.uka.ilkd.key.logic.Namespace;
026: import de.uka.ilkd.key.logic.NamespaceSet;
027: import de.uka.ilkd.key.logic.Term;
028: import de.uka.ilkd.key.logic.op.ProgramMethod;
029: import de.uka.ilkd.key.logic.op.ProgramVariable;
030:
031: /** A normal jml methodspecification declared by the jml-keyword
032: <code>normal_behavior</code>*/
033: public class JMLNormalMethodSpec extends JMLMethodSpec {
034:
035: public JMLNormalMethodSpec(ProgramMethod pm, Services services,
036: Namespace params, LinkedHashMap term2old,
037: JMLClassSpec cSpec, NamespaceSet nss, String javaPath) {
038:
039: super (pm, services, params, term2old, cSpec, nss, javaPath);
040: addSignals(exc, null, ff());
041:
042: }
043:
044: protected JMLNormalMethodSpec() {
045: super ();
046: }
047:
048: /**
049: * This is used for modelling specification inheritance for overwriten
050: * methods.
051: */
052: public JMLMethodSpec cloneFor(ProgramMethod method,
053: JMLClassSpec jmlClassSpec) {
054: if (!isCloneableFor(method))
055: return null;
056: JMLNormalMethodSpec cloned = new JMLNormalMethodSpec();
057: return cloneForHelper(cloned, method, jmlClassSpec);
058: }
059:
060: public ProgramElement getProofStatement() {
061: return makeMBS().getStatementAt(0);
062: }
063:
064: protected Term createModalityTermForEnsures(Term post,
065: boolean desugar, boolean withInv, boolean allInv) {
066: ModTermKey key = new ModTermKey(post, desugar, withInv, allInv);
067: Term c = (Term) modalityTermForEnsuresCache.get(key);
068: if (c != null) {
069: return c;
070: }
071: if (diverges == null || ff().equals(diverges)) {
072: JavaBlock jb = JavaBlock
073: .createJavaBlock(new StatementBlock(makeMBS()));
074: if (withInv
075: && !services.getImplementation2SpecMap()
076: .getModifiers(pm).contains("helper")) {
077: post = cSpec.addClassSpec2Post(post, true, !allInv, pm,
078: cSpec);
079: if (allInv) {
080: Term ai = UsefulTools.allInvariants(services
081: .getImplementation2SpecMap());
082: if (ai != null) {
083: post = and(ai, post);
084: }
085: }
086: }
087: post = updatePrefix(post);
088: post = UsefulTools.addRepresents(post, services,
089: (ProgramVariable) cSpec.getInstancePrefix());
090: c = dia(jb, post);
091: } else {
092: final Term excVarTerm = var(excVar);
093: post = and(equals(excVarTerm, nullTerm), post);
094: final JavaBlock jb = catchAllJB(desugar);
095:
096: if (withInv
097: && !services.getImplementation2SpecMap()
098: .getModifiers(pm).contains("helper")) {
099: post = cSpec.addClassSpec2Post(post, true, !allInv, pm,
100: cSpec);
101: if (allInv) {
102: Term ai = UsefulTools.allInvariants(services
103: .getImplementation2SpecMap());
104: if (ai != null) {
105: post = and(ai, post);
106: }
107: }
108: }
109: post = updatePrefix(post);
110: post = UsefulTools.addRepresents(post, services,
111: (ProgramVariable) cSpec.getInstancePrefix());
112: c = box(jb, post);
113: }
114: modalityTermForEnsuresCache.put(key, c);
115: return c;
116: }
117:
118: public JMLMethodSpec copy() {
119: final JMLNormalMethodSpec copy = new JMLNormalMethodSpec(pm,
120: services, params, term2old, cSpec, nss, getJavaPath());
121: return copyHelper(copy);
122: }
123:
124: public String toString() {
125: return toStringHelper("normal_behavior speccase");
126: }
127: }
|