01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16:
17: package de.uka.ilkd.key.jml;
18:
19: import java.util.LinkedHashMap;
20:
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.java.abstraction.Constructor;
23: import de.uka.ilkd.key.logic.Namespace;
24: import de.uka.ilkd.key.logic.NamespaceSet;
25: import de.uka.ilkd.key.logic.Term;
26: import de.uka.ilkd.key.logic.op.ProgramMethod;
27:
28: public class JMLExceptionalMethodSpec extends JMLMethodSpec {
29:
30: public JMLExceptionalMethodSpec(ProgramMethod md,
31: Services services, Namespace params,
32: LinkedHashMap term2old, JMLClassSpec cSpec,
33: NamespaceSet nss, String javaPath) {
34: super (md, services, params, term2old, cSpec, nss, javaPath);
35: }
36:
37: protected JMLExceptionalMethodSpec() {
38: super ();
39: }
40:
41: /**
42: * This is used for modelling specification inheritance for overwriten
43: * methods.
44: */
45: public JMLMethodSpec cloneFor(ProgramMethod md,
46: JMLClassSpec jmlClassSpec) {
47: if (!isCloneableFor(md))
48: return null;
49: JMLExceptionalMethodSpec cloned = new JMLExceptionalMethodSpec();
50: return cloneForHelper(cloned, md, jmlClassSpec);
51: }
52:
53: public void addPost(Term t) {
54: }
55:
56: public Term getPost() {
57: return ff();
58: }
59:
60: public JMLMethodSpec copy() {
61: JMLExceptionalMethodSpec copy = new JMLExceptionalMethodSpec(
62: pm, services, params, term2old, cSpec, nss,
63: getJavaPath());
64: return copyHelper(copy);
65: }
66:
67: public String toString() {
68: return toStringHelper("exceptional_behavior speccase");
69: }
70:
71: public Term getCompletePost(boolean withClassSpec, boolean allInv) {
72: if (lv2old == null) {
73: getPi1();
74: }
75: Term result = createModalityTermForEnsures(ff(), false,
76: withClassSpec, allInv).sub(0);
77: result = addOldQuantifiers(result, lv2old, false, params);
78: if (!(pm.getMethodDeclaration() instanceof Constructor)) {
79: result = updatePrefix(result);
80: }
81: return result;
82: }
83:
84: }
|