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: //
09: //
10:
11: /* Generated by Together */
12:
13: package de.uka.ilkd.key.casetool;
14:
15: import de.uka.ilkd.key.proof.mgt.Contractable;
16: import de.uka.ilkd.key.speclang.ListOfOperationContract;
17:
18: public interface ModelMethod extends ReprModel, Contractable {
19:
20: ModelClass getContainingClass();
21:
22: String getContainingClassName();
23:
24: String getContainingPackage();
25:
26: // return signature of form name(arg1: type1; arg2: type2 ...)
27: // and translates Java types to OCL types
28: String getCallSignature();
29:
30: // return signature of form name(arg1: type1; arg2: type2 ...)
31: String getCallSignature(boolean translateJavaType2OCLTypes);
32:
33: int getNumParameters();
34:
35: String getParameterNameAt(int i);
36:
37: String getParameterTypeAt(int i);
38:
39: String getResultType();
40:
41: String getName();
42:
43: boolean isVoid();
44:
45: boolean isConstructor();
46:
47: boolean isPrivate();
48:
49: // returns precondition if any, else ""
50: String getMyPreCond();
51:
52: // returns modifies clause if any, else ""
53: String getMyModifClause();
54:
55: // set modifies clause
56: void setMyModifClause(String modifClause);
57:
58: boolean isQuery();
59:
60: // set precondition
61: void setMyPreCond(String precond);
62:
63: // returns precondition of parent if any, else ""
64: String getParentPreCond();
65:
66: String getMyPostCond();
67:
68: ModelMethod getParentMethod();
69:
70: void setMyPostCond(String postcond);
71:
72: String getParentPostCond();
73:
74: // set/get GF abstract syntax representation of pre-/postconditions
75: String getMyGFAbs();
76:
77: void setMyGFAbs(String abs);
78:
79: boolean hasOrigParent();
80:
81: ListOfOperationContract getMyOperationContracts();
82: }
|