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.jml;
19:
20: import de.uka.ilkd.key.java.Services;
21: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
22: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
23: import de.uka.ilkd.key.logic.op.ParsableVariable;
24: import de.uka.ilkd.key.speclang.FormulaWithAxioms;
25:
26: /**
27: * Translates JML expressions to DL.
28: */
29: public class JMLTranslator {
30: private final Services services;
31:
32: public JMLTranslator(Services services) {
33: this .services = services;
34: }
35:
36: public FormulaWithAxioms translateRequires(String requires,
37: ParsableVariable selfVar, ListOfParsableVariable paramVars) {
38: return null;//TODO
39: }
40:
41: public FormulaWithAxioms translateEnsures(String ensures,
42: ParsableVariable selfVar, ListOfParsableVariable paramVars,
43: ParsableVariable resultVar, ParsableVariable excVar) {
44: return null;//TODO
45: }
46:
47: public FormulaWithAxioms translateSignals(String signals,
48: ParsableVariable selfVar, ListOfParsableVariable paramVars,
49: ParsableVariable resultVar, ParsableVariable excVar) {
50: return null;//TODO
51: }
52:
53: public FormulaWithAxioms translateDiverges(String diverges,
54: ParsableVariable selfVar, ListOfParsableVariable paramVars) {
55: return null;//TODO
56: }
57:
58: public SetOfLocationDescriptor translateAssignable(String modifies,
59: ParsableVariable selfVar, ListOfParsableVariable paramVars) {
60: return null;//TODO
61: }
62:
63: public FormulaWithAxioms translateInv(String inv,
64: ParsableVariable selfVar) {
65: return null;//TODO
66: }
67: }
|