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: //
10:
11: package de.uka.ilkd.key.proof.mgt;
12:
13: import de.uka.ilkd.key.casetool.ModelMethod;
14:
15: public class ContractUtil {
16:
17: private ContractUtil() {
18: }
19:
20: public static PrePostPair getPreInvPost(ModelMethod m) {
21: String pre = "("
22: + normalizeConstraint(m.getMyPreCond())
23: + ")"
24: + " and "
25: + "("
26: + normalizeConstraint(m.getContainingClass().getMyInv())
27: + ")";
28: String post = normalizeConstraint(m.getMyPostCond());
29: return new PrePostPair(pre, post);
30: }
31:
32: public static PrePostPair getPrePost(ModelMethod m) {
33: String pre = "(" + normalizeConstraint(m.getMyPreCond()) + ")";
34: String post = normalizeConstraint(m.getMyPostCond());
35: pre = pre.trim();
36: post = post.trim();
37: return new PrePostPair(pre, post);
38: }
39:
40: public static PrePostPair getPreInvPostInv(ModelMethod m) {
41: String inv = normalizeConstraint(m.getContainingClass()
42: .getMyInv());
43: String pre = "(" + normalizeConstraint(m.getMyPreCond()) + ")"
44: + " and " + "(" + inv + ")";
45: String post = "(" + normalizeConstraint(m.getMyPostCond())
46: + ")" + " and " + "(" + inv + ")";
47: return new PrePostPair(pre, post);
48: }
49:
50: public static PrePostPair getPreInvInv(ModelMethod m) {
51: String inv = normalizeConstraint(m.getContainingClass()
52: .getMyInv());
53: String pre = "(" + normalizeConstraint(m.getMyPreCond()) + ")"
54: + " and " + "(" + inv + ")";
55: return new PrePostPair(pre, inv);
56: }
57:
58: public static PrePostPair getPreInvTout(ModelMethod m) {
59: String poToutText;
60: if (m.getContainingClassName().equals(m.getName())) {
61: poToutText = "";
62: } else {
63: poToutText = "("
64: + normalizeConstraint(m.getMyPreCond())
65: + ")"
66: + " and "
67: + "("
68: + normalizeConstraint(m.getContainingClass()
69: .getMyInv())
70: + ")"
71: + " and "
72: + "("
73: + normalizeConstraint(m.getContainingClass()
74: .getMyThroughout()) + ")";
75: }
76: return new PrePostPair(poToutText, normalizeConstraint(m
77: .getContainingClass().getMyThroughout()));
78: }
79:
80: /**
81: * Converts an empty string to "true" and keeps it unchanged otherwise.
82: */
83: public static String normalizeConstraint(String aText) {
84: if (aText.equals("")) {
85: return "true";
86: } else {
87: return aText;
88: }
89: }
90:
91: }
|