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;
19:
20: import de.uka.ilkd.key.casetool.ModelClass;
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
23: import de.uka.ilkd.key.logic.TermBuilder;
24:
25: public abstract class AbstractClassInvariant implements ClassInvariant {
26: protected static final TermBuilder tb = TermBuilder.DF;
27: private final ModelClass modelClass;
28:
29: public AbstractClassInvariant(ModelClass modelClass) {
30: this .modelClass = modelClass;
31: }
32:
33: public ModelClass getModelClass() {
34: return modelClass;
35: }
36:
37: public KeYJavaType getKJT(Services services) {
38: return services.getJavaInfo().getTypeByClassName(
39: modelClass.getFullClassName());
40: }
41: }
|