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: package de.uka.ilkd.key.proof.mgt;
10:
11: import de.uka.ilkd.key.proof.Proof;
12: import de.uka.ilkd.key.rule.Rule;
13:
14: public class DepAnalysis {
15:
16: private final boolean depExists;
17: private final Rule r;
18: private final Proof p;
19: private final String info;
20:
21: private static final DepAnalysis noDepInstance = new DepAnalysis(
22: false, "No Dependency");
23:
24: public static DepAnalysis getInstance(boolean depExists, Rule r,
25: Proof p, String info) {
26: if (!depExists) {
27: return noDepInstance;
28: } else {
29: return new DepAnalysis(depExists, r, p, info);
30: }
31: }
32:
33: public static DepAnalysis getInstance(boolean depExists, Rule r,
34: Proof p) {
35: return getInstance(depExists, r, p, "");
36: }
37:
38: public static DepAnalysis getInstance(boolean depExists, String info) {
39: return getInstance(depExists, null, null, info);
40: }
41:
42: private DepAnalysis(boolean depExists, Rule r, Proof p, String info) {
43: this .depExists = depExists;
44: this .r = r;
45: this .p = p;
46: this .info = info;
47: }
48:
49: public DepAnalysis(boolean depExists, String info) {
50: this (depExists, null, null, info);
51: }
52:
53: public String toString() {
54: StringBuffer res = null;
55: if (r != null && p != null) {
56: res = new StringBuffer("Rule " + r.name() + " is ");
57: if (depExists)
58: res.append("not ");
59: res.append("used in proof " + p.name() + ". ");
60: }
61: return (res != null) ? res + info : info;
62: }
63:
64: public boolean depExists() {
65: return depExists;
66: }
67:
68: }
|