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.ocl;
19:
20: import de.uka.ilkd.key.casetool.ModelMethod;
21: import de.uka.ilkd.key.java.Services;
22: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
23: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
24: import de.uka.ilkd.key.logic.op.Modality;
25: import de.uka.ilkd.key.logic.op.ParsableVariable;
26: import de.uka.ilkd.key.speclang.AbstractOperationContract;
27: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
28: import de.uka.ilkd.key.speclang.SLTranslationError;
29:
30: public class OCLOperationContract extends AbstractOperationContract {
31: private final String originalPre;
32: private final String originalPost;
33: private final String originalModifies;
34:
35: public OCLOperationContract(ModelMethod modelMethod,
36: boolean terminationRequired, String originalPre,
37: String originalPost, String originalModifies) {
38: super (modelMethod, terminationRequired ? Modality.DIA
39: : Modality.BOX);
40: this .originalPre = originalPre;
41: this .originalPost = originalPost;
42: this .originalModifies = originalModifies;
43: }
44:
45: public FormulaWithAxioms getPre(ParsableVariable selfVar,
46: ListOfParsableVariable paramVars, Services services)
47: throws SLTranslationError {
48: return services.getOCLTranslator().translatePre(originalPre,
49: selfVar, paramVars);
50: }
51:
52: public FormulaWithAxioms getPost(ParsableVariable selfVar,
53: ListOfParsableVariable paramVars,
54: ParsableVariable resultVar, ParsableVariable excVar,
55: Services services) throws SLTranslationError {
56: return services.getOCLTranslator().translatePost(originalPost,
57: selfVar, paramVars, resultVar, excVar);
58: }
59:
60: public SetOfLocationDescriptor getModifies(
61: ParsableVariable selfVar, ListOfParsableVariable paramVars,
62: Services services) throws SLTranslationError {
63: return services.getOCLTranslator().translateModifies(
64: originalModifies, selfVar, paramVars);
65: }
66: }
|