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.ModelMethod;
21: import de.uka.ilkd.key.java.JavaInfo;
22: import de.uka.ilkd.key.java.Services;
23: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
24: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
25: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
26: import de.uka.ilkd.key.logic.TermBuilder;
27: import de.uka.ilkd.key.logic.op.Modality;
28: import de.uka.ilkd.key.logic.op.ProgramMethod;
29:
30: public abstract class AbstractOperationContract implements
31: OperationContract {
32: protected static final TermBuilder tb = TermBuilder.DF;
33: private final ModelMethod modelMethod;
34: private final Modality modality;
35:
36: public AbstractOperationContract(ModelMethod modelMethod,
37: Modality modality) {
38: this .modelMethod = modelMethod;
39: this .modality = modality;
40: }
41:
42: public ModelMethod getModelMethod() {
43: return modelMethod;
44: }
45:
46: public ProgramMethod getProgramMethod(Services services) {
47: JavaInfo javaInfo = services.getJavaInfo();
48:
49: String containingClassName = modelMethod
50: .getContainingClassName();
51: KeYJavaType containingClass = javaInfo
52: .getKeYJavaTypeByClassName(containingClassName);
53:
54: ListOfKeYJavaType signature = SLListOfKeYJavaType.EMPTY_LIST;
55: for (int i = 0; i < modelMethod.getNumParameters(); i++) {
56: String parTypeName = modelMethod.getParameterTypeAt(i);
57: signature = signature.append(javaInfo
58: .getKeYJavaType(parTypeName));
59: }
60:
61: return javaInfo.getProgramMethod(containingClass, modelMethod
62: .getName(), signature, javaInfo.getJavaLangObject());
63: }
64:
65: public Modality getModality() {
66: return modality;
67: }
68: }
|