001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.mgt;
012:
013: import java.util.HashSet;
014: import java.util.Iterator;
015: import java.util.Set;
016: import java.util.Vector;
017:
018: import de.uka.ilkd.key.casetool.*;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
021: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
022: import de.uka.ilkd.key.speclang.SLListOfClassInvariant;
023:
024: public class JavaModelClass implements ModelClass {
025:
026: private final KeYJavaType kjt;
027: private final String rootDir;
028: private final Services services;
029:
030: public JavaModelClass(KeYJavaType kjt, String rootDir,
031: Services services) {
032: assert kjt != null;
033: assert rootDir != null;
034: this .kjt = kjt;
035: this .rootDir = rootDir;
036: this .services = services;
037: }
038:
039: public KeYJavaType getKeYJavaType() {
040: return kjt;
041: }
042:
043: public String getClassName() {
044: return kjt.getJavaType().getName();
045: }
046:
047: public String getFullClassName() {
048: return kjt.getJavaType().getFullName();
049: }
050:
051: // returns the invariant of the class if any, else ""
052: public String getMyInv() {
053: return "";//%%
054: }
055:
056: // returns the throughout of the class if any, else ""
057: public String getMyThroughout() {
058: return "";//%%
059:
060: }
061:
062: // set the (OCL) invariant of the class
063: public void setMyInv(String inv) {
064:
065: }
066:
067: // set the GF abstract syntax for the invariant of the class
068: public void setMyInvGFAbs(String inv) {
069:
070: }
071:
072: // get the GF abstract syntax for the invariant of the class
073: public String getMyInvGFAbs() {
074: return "";//%%
075:
076: }
077:
078: //returns the package containing this class. If there
079: // is none, returns null
080: public String getContainingPackage() {
081: String classname = kjt.getFullName();
082: if (classname.indexOf(".") >= 0) {
083: return classname.substring(0, classname.lastIndexOf("."));
084: } else {
085: return null;
086: }
087: }
088:
089: // return the invariant of the parent if any, else ""
090: public String getParentInv() {
091: return "";//%%
092:
093: }
094:
095: // return the classname of the parent if any, else ""
096: public String getParentClassName() {
097:
098: return "";//%%
099: }
100:
101: // returns true if class has a parent
102: public boolean hasOrigParent() {
103: return false;
104: }
105:
106: // calls getOpNames on parent if any, else returns null
107: public Vector getParentOpNames() {
108: return null;
109: }
110:
111: // calls getOps on parent if any, else returns null
112: public Vector getParentOps() {
113: return null;
114: }
115:
116: // calls getOpNames on parent if any, else returns null
117: public Vector getInheritedOpNames() {
118: return null;
119: }
120:
121: // calls getOps on parent if any, else returns null
122: public Vector getInheritedOps() {
123: return null;
124: }
125:
126: public Vector getOpNames() {
127: return null;
128:
129: }
130:
131: // returns ReprModelMethod
132: public Vector getOps() {
133:
134: return null;
135: }
136:
137: public void getAssociations(HashMapOfClassifier classifiers) {
138:
139: }
140:
141: public String getText() {
142: return "";//%%
143: }
144:
145: public String[] getClassesInPackage() {
146: return new String[0];
147: }
148:
149: public String getRootDirectory() {
150: return rootDir;
151: }
152:
153: public Set getAllClasses() {
154: Set allKJTs = services.getJavaInfo().getAllKeYJavaTypes();
155: Iterator it = allKJTs.iterator();
156: Set result = new HashSet();
157: while (it.hasNext()) {
158: result.add(new JavaModelClass((KeYJavaType) it.next(),
159: rootDir, services));
160: }
161: return result;
162: }
163:
164: public String getActXmifile() {
165: return "";
166: }
167:
168: public int hashCode() {
169: int result = 7;
170: result = 13 * result + getKeYJavaType().hashCode();
171: result = 13 * result + getRootDirectory().hashCode();
172: return result;
173: }
174:
175: public boolean equals(Object o) {
176: if (!(o instanceof JavaModelClass)) {
177: return false;
178: }
179: JavaModelClass cmp = (JavaModelClass) o;
180: return kjt.equals(cmp.getKeYJavaType())
181: && getRootDirectory().equals(cmp.getRootDirectory());
182: }
183:
184: public ListOfClassInvariant getMyClassInvariants() {
185: return services.getSpecificationRepository()
186: .getAllInvariantsForType(getKeYJavaType());
187: }
188:
189: public ListOfClassInvariant getMyThroughoutClassInvariants() {
190: return SLListOfClassInvariant.EMPTY_LIST;//%%
191: }
192:
193: public ListOfModelClass getMyParents() {
194: return SLListOfModelClass.EMPTY_LIST;//%
195: }
196:
197: public UMLInfo createUMLInfo(Services services) {
198: return new UMLInfo(services, SLListOfAssociation.EMPTY_LIST);//%
199: }
200:
201: public String toString() {
202: return getKeYJavaType() + "," + getRootDirectory();
203: }
204: }
|