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.java;
012:
013: import java.util.HashMap;
014: import java.util.Iterator;
015:
016: import de.uka.ilkd.key.casetool.UMLInfo;
017: import de.uka.ilkd.key.java.recoderext.KeYCrossReferenceServiceConfiguration;
018: import de.uka.ilkd.key.java.recoderext.SchemaCrossReferenceServiceConfiguration;
019: import de.uka.ilkd.key.jml.Implementation2SpecMap;
020: import de.uka.ilkd.key.logic.InnerVariableNamer;
021: import de.uka.ilkd.key.logic.NamespaceSet;
022: import de.uka.ilkd.key.logic.VariableNamer;
023: import de.uka.ilkd.key.proof.Counter;
024: import de.uka.ilkd.key.proof.Node;
025: import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
026: import de.uka.ilkd.key.speclang.jml.JMLTranslator;
027: import de.uka.ilkd.key.speclang.ocl.OCLTranslator;
028: import de.uka.ilkd.key.util.Debug;
029: import de.uka.ilkd.key.util.KeYExceptionHandler;
030: import de.uka.ilkd.key.util.KeYRecoderExcHandler;
031:
032: /**
033: * this is a collection of common services to the KeY prover. Services
034: * include information on the underlying Java model and a converter to
035: * transform Java program elements to logic (where possible) and back.
036: */
037: public class Services {
038:
039: /**
040: * proof specific namespaces (functions, predicates, sorts, variables)
041: */
042: private NamespaceSet namespaces = new NamespaceSet();
043:
044: /** used to determine whether an expression is a compile-time
045: * constant and if so the type and result of the expression
046: */
047: private ConstantExpressionEvaluator cee;
048:
049: /** used to convert types, expressions and so on to logic elements
050: * (in special into to terms or formulas)
051: */
052: private TypeConverter typeconverter;
053:
054: /**
055: * the information object on the Java model
056: */
057: private JavaInfo javainfo;
058:
059: /**
060: * The information object on the UML model
061: */
062: private UMLInfo umlinfo;
063:
064: /**
065: * a translator for OCL expressions
066: */
067: private final OCLTranslator oclTranslator = new OCLTranslator(this );
068:
069: /**
070: * a translator for JML expressions
071: */
072: private final JMLTranslator jmlTranslator = new JMLTranslator(this );
073:
074: /**
075: * mapping for jml specifications
076: * @deprecated
077: */
078: private Implementation2SpecMap specMap;
079:
080: /**
081: * variable namer for inner renaming
082: */
083: private VariableNamer innerVarNamer = new InnerVariableNamer(this );
084:
085: /**
086: * the exception-handler
087: */
088: private KeYExceptionHandler exceptionHandler;
089:
090: /**
091: * map of names to counters
092: */
093: private HashMap counters = new HashMap();
094:
095: private SpecificationRepository specRepos;
096:
097: /**
098: * creates a new Services object with a new TypeConverter and a new
099: * JavaInfo object with no information stored at none of these.
100: */
101: public Services(KeYExceptionHandler exceptionHandler) {
102: cee = new ConstantExpressionEvaluator(this );
103: typeconverter = new TypeConverter(this );
104: if (exceptionHandler == null) {
105: this .exceptionHandler = new KeYRecoderExcHandler();
106: } else {
107: this .exceptionHandler = exceptionHandler;
108: }
109: javainfo = new JavaInfo(new KeYProgModelInfo(typeconverter,
110: exceptionHandler), this );
111: specMap = new Implementation2SpecMap(this );
112: specRepos = new SpecificationRepository(this );
113: }
114:
115: public Services() {
116: this ((KeYExceptionHandler) null);
117: }
118:
119: private Services(KeYCrossReferenceServiceConfiguration crsc,
120: KeYRecoderMapping rec2key) {
121: cee = new ConstantExpressionEvaluator(this );
122: typeconverter = new TypeConverter(this );
123: // exceptionHandler = new KeYRecoderExcHandler();
124: javainfo = new JavaInfo(new KeYProgModelInfo(crsc, rec2key,
125: typeconverter), this );
126: }
127:
128: /** THIS CONSTRUCTOR IS ONLY FOR TESTS!
129: * creates a Services object that contains the given JavaInfo object, a
130: * type converter is created
131: * @param ji the JavaInfo to use
132: */
133: public Services(JavaInfo ji) {
134: javainfo = ji;
135: typeconverter = new TypeConverter(this );
136: specMap = new Implementation2SpecMap(this );
137: specRepos = new SpecificationRepository(this );
138: exceptionHandler = new KeYRecoderExcHandler();
139: }
140:
141: public KeYExceptionHandler getExceptionHandler() {
142: return exceptionHandler;
143: }
144:
145: public void setExceptionHandler(KeYExceptionHandler keh) {
146: exceptionHandler = keh;
147: }
148:
149: /**
150: * Returns the TypeConverter associated with this Services object.
151: */
152: public TypeConverter getTypeConverter() {
153: return typeconverter;
154: }
155:
156: private void setTypeConverter(TypeConverter tc) {
157: typeconverter = tc;
158: }
159:
160: /**
161: * Returns the ConstantExpressionEvaluator associated with this Services object.
162: */
163: public ConstantExpressionEvaluator getConstantExpressionEvaluator() {
164: return cee;
165: }
166:
167: /**
168: * Returns the JavaInfo associated with this Services object.
169: */
170: public JavaInfo getJavaInfo() {
171: return javainfo;
172: }
173:
174: /**
175: * Returns the UMLInfo associated with this Services object.
176: */
177: public UMLInfo getUMLInfo() {
178: return umlinfo;
179: }
180:
181: public void setUMLInfo(UMLInfo umlinfo) {
182: this .umlinfo = umlinfo;
183: }
184:
185: public SpecificationRepository getSpecificationRepository() {
186: return specRepos;
187: }
188:
189: /**
190: * Returns the VariableNamer associated with this Services object.
191: */
192: public VariableNamer getVariableNamer() {
193: return innerVarNamer;
194: }
195:
196: public OCLTranslator getOCLTranslator() {
197: return oclTranslator;
198: }
199:
200: public JMLTranslator getJMLTranslator() {
201: return jmlTranslator;
202: }
203:
204: /**
205: * Returns the Implementation2SpecMap associated with this Services object.
206: * @deprecated
207: */
208: public Implementation2SpecMap getImplementation2SpecMap() {
209: return specMap;
210: }
211:
212: private void setImplementation2SpecMap(Implementation2SpecMap map) {
213: specMap = map;
214: }
215:
216: /**
217: * creates a new services object containing a copy of the java info of
218: * this object and a new TypeConverter (shallow copy)
219: * @return the copy
220: */
221: public Services copy() {
222: Debug
223: .assertTrue(
224: !(getJavaInfo().getKeYProgModelInfo()
225: .getServConf() instanceof SchemaCrossReferenceServiceConfiguration),
226: "services: tried to copy schema cross reference service config.");
227: Services s = new Services(getJavaInfo().getKeYProgModelInfo()
228: .getServConf(), getJavaInfo().getKeYProgModelInfo()
229: .rec2key().copy());
230: s.setTypeConverter(getTypeConverter().copy(s));
231: s.setImplementation2SpecMap(specMap.copy(s));
232: s.specRepos = specRepos.copy(s);
233: s.setExceptionHandler(getExceptionHandler());
234: s.setNamespaces(namespaces.copy());
235: return s;
236: }
237:
238: /**
239: * creates a new service object with the same ldt information
240: * as the actual one
241: */
242: public Services copyPreservesLDTInformation() {
243: Debug
244: .assertTrue(
245: !(javainfo.getKeYProgModelInfo().getServConf() instanceof SchemaCrossReferenceServiceConfiguration),
246: "services: tried to copy schema cross reference service config.");
247: Services s = new Services(getExceptionHandler());
248: s.setTypeConverter(getTypeConverter().copy(s));
249: s.setImplementation2SpecMap(specMap.copy(s));
250: s.specRepos = specRepos.copy(s);
251: s.setNamespaces(namespaces.copy());
252: return s;
253: }
254:
255: public Services copyProofSpecific() {
256: final Services s = new Services(getJavaInfo()
257: .getKeYProgModelInfo().getServConf(), getJavaInfo()
258: .getKeYProgModelInfo().rec2key());
259: s.setTypeConverter(getTypeConverter().copy(s));
260: s.setImplementation2SpecMap(specMap.copy(s));
261: s.setExceptionHandler(getExceptionHandler());
262: s.setNamespaces(namespaces.copy());
263: s.specRepos = specRepos;
264: return s;
265: }
266:
267: /*
268: * returns an existing named counter, creates a new one otherwise
269: */
270: public Counter getCounter(String name) {
271: Counter c = (Counter) counters.get(name);
272: if (c != null)
273: return c;
274: c = new Counter(name);
275: counters.put(name, c);
276: return c;
277: }
278:
279: public void setBackCounters(Node n) {
280: Iterator it = counters.values().iterator();
281: while (it.hasNext())
282: ((Counter) it.next()).undo(n);
283: }
284:
285: /**
286: * returns the namespaces for functions, predicates etc.
287: * @return the proof specific namespaces
288: */
289: public NamespaceSet getNamespaces() {
290: return namespaces;
291: }
292:
293: /**
294: * sets the namespaces of known predicates, functions, variables
295: * @param namespaces the NamespaceSet with the proof specific namespaces
296: */
297: public void setNamespaces(NamespaceSet namespaces) {
298: this.namespaces = namespaces;
299: }
300: }
|