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: package de.uka.ilkd.key.speclang;
09:
10: import java.io.IOException;
11:
12: import de.uka.ilkd.key.casetool.ModelClass;
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.op.ParsableVariable;
16: import de.uka.ilkd.key.pp.LogicPrinter;
17: import de.uka.ilkd.key.pp.NotationInfo;
18: import de.uka.ilkd.key.pp.ProgramPrinter;
19:
20: /**
21: * @deprecated
22: */
23: public class TranslatedClassInvariant extends AbstractClassInvariant {
24:
25: private final Term translation;
26: private final Services services;
27:
28: /**
29: * Creates a class invariant.
30: * @param modelClass the invariant's model class
31: * @param inv the invariant in some specification language
32: * @param translator a suitable translator for expressions of this
33: * specification language
34: */
35: public TranslatedClassInvariant(ModelClass modelClass,
36: Term translation, Services services) {
37: super (modelClass);
38: this .translation = translation;
39: this .services = services;
40: }
41:
42: public FormulaWithAxioms getInv(Services services) {
43: return new FormulaWithAxioms(translation);
44: }
45:
46: public FormulaWithAxioms getOpenInv(ParsableVariable selfVar,
47: Services services) {
48: //not implemented
49: assert false;
50: return null;
51: }
52:
53: public String toString() {
54: LogicPrinter p = new LogicPrinter(new ProgramPrinter(),
55: NotationInfo.createInstance(), services);
56: try {
57: p.printTerm(translation);
58: } catch (IOException ioe) {
59: return translation.toString();
60: }
61: return p.result().toString();
62: }
63: }
|