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.casetool;
09:
10: import java.util.Set;
11: import java.util.Vector;
12:
13: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
14:
15: public interface ModelClass {
16:
17: public abstract String getClassName();
18:
19: public abstract String getFullClassName();
20:
21: // returns the invariant of the class if any, else ""
22: public abstract String getMyInv();
23:
24: // returns the throughout of the class if any, else ""
25: public abstract String getMyThroughout();
26:
27: // get the GF abstract syntax for the invariant of the class
28: public abstract String getMyInvGFAbs();
29:
30: //returns the package containing this class. If there
31: // is none, returns null
32: public abstract String getContainingPackage();
33:
34: public abstract String[] getClassesInPackage();
35:
36: public abstract String getRootDirectory();
37:
38: /**
39: * Returns all supertypes of the class, including implemented interfaces.
40: */
41: ListOfModelClass getMyParents();
42:
43: // returns ReprModelMethod
44: Vector getOps();
45:
46: public abstract Set getAllClasses();
47:
48: /**
49: * Returns the invariants of the class.
50: */
51: public abstract ListOfClassInvariant getMyClassInvariants();
52:
53: /**
54: * Returns the throughout invariants of the class.
55: */
56: public abstract ListOfClassInvariant getMyThroughoutClassInvariants();
57:
58: }
|