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.ocl;
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.Term;
24: import de.uka.ilkd.key.logic.op.LogicVariable;
25: import de.uka.ilkd.key.logic.op.Op;
26: import de.uka.ilkd.key.logic.op.ParsableVariable;
27: import de.uka.ilkd.key.logic.sort.Sort;
28: import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory;
29: import de.uka.ilkd.key.speclang.AbstractClassInvariant;
30: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
31: import de.uka.ilkd.key.speclang.SLTranslationError;
32:
33: public class OCLClassInvariant extends AbstractClassInvariant {
34: private final String originalInv;
35:
36: public OCLClassInvariant(ModelClass modelClass, String originalInv) {
37: super (modelClass);
38: this .originalInv = originalInv;
39: }
40:
41: public FormulaWithAxioms getInv(Services services)
42: throws SLTranslationError {
43: Sort sort = getKJT(services).getSort();
44: LogicVariable selfVar = new LogicVariable(new Name("self"),
45: sort);
46:
47: FormulaWithAxioms inv = services.getOCLTranslator()
48: .translateInv(originalInv, selfVar);
49:
50: CreatedAttributeTermFactory catf = CreatedAttributeTermFactory.INSTANCE;
51: Term closedInv = catf.createCreatedNotNullQuantifierTerm(
52: services, Op.ALL, selfVar, inv.getFormula());
53:
54: return new FormulaWithAxioms(closedInv, inv.getAxioms());
55: }
56:
57: public FormulaWithAxioms getOpenInv(ParsableVariable selfVar,
58: Services services) throws SLTranslationError {
59: return services.getOCLTranslator().translateInv(originalInv,
60: selfVar);
61: }
62:
63: public String toString() {
64: return originalInv;
65: }
66:
67: public boolean equals(Object o) {
68: if (!(o instanceof OCLClassInvariant)) {
69: return false;
70: }
71: return originalInv.equals(((OCLClassInvariant) o).originalInv);
72: }
73:
74: public int hashCode() {
75: return originalInv.hashCode();
76: }
77: }
|