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: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // 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:
18: package de.uka.ilkd.key.speclang.jml;
19:
20: import de.uka.ilkd.key.casetool.ModelClass;
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.logic.Name;
23: import de.uka.ilkd.key.logic.op.LogicVariable;
24: import de.uka.ilkd.key.logic.op.ParsableVariable;
25: import de.uka.ilkd.key.logic.sort.Sort;
26: import de.uka.ilkd.key.speclang.AbstractClassInvariant;
27: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
28:
29: public class JMLClassInvariant extends AbstractClassInvariant {
30: private final String originalInv;
31:
32: public JMLClassInvariant(ModelClass modelClass, String originalInv) {
33: super (modelClass);
34: this .originalInv = originalInv;
35: }
36:
37: public FormulaWithAxioms getInv(Services services) {
38: Sort sort = getKJT(services).getSort();
39: String name = sort.name().toString().substring(0, 0)
40: .toLowerCase();
41: LogicVariable selfVar = new LogicVariable(new Name(name), sort);
42:
43: FormulaWithAxioms inv = services.getJMLTranslator()
44: .translateInv(originalInv, selfVar);
45:
46: return new FormulaWithAxioms(tb.all(selfVar, inv.getFormula()),
47: inv.getAxioms());
48: }
49:
50: public FormulaWithAxioms getOpenInv(ParsableVariable selfVar,
51: Services services) {
52: return services.getJMLTranslator().translateInv(originalInv,
53: selfVar);
54: }
55:
56: public String toString() {
57: return originalInv;
58: }
59:
60: public boolean equals(Object o) {
61: if (!(o instanceof JMLClassInvariant)) {
62: return false;
63: }
64: return originalInv.equals(((JMLClassInvariant) o).originalInv);
65: }
66:
67: public int hashCode() {
68: return originalInv.hashCode();
69: }
70: }
|