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.strategy;
012:
013: import de.uka.ilkd.key.logic.Name;
014:
015: /**
016: * Parametrize the strategy Simple JavaCardDL to get rid of that messy class
017: * hierarchy. Someone write a GUI for this class ...
018: */
019: public abstract class SimpleJavaCardDLOptions {
020:
021: protected final static String BASE_NAME = "Simple JavaCardDL";
022:
023: public abstract Name name();
024:
025: public boolean useMethodContracts() {
026: return false;
027: }
028:
029: public boolean unwindLoops() {
030: return false;
031: }
032:
033: public boolean expandMethods() {
034: return false;
035: }
036:
037: public boolean test() {
038: return false;
039: }
040:
041: public static final SimpleJavaCardDLOptions NOTHING = new SimpleJavaCardDLOptions() {
042: public Name name() {
043: return new Name(BASE_NAME
044: + " without expanding loops and method bodies");
045: }
046: };
047:
048: public static final SimpleJavaCardDLOptions LOOPS = new SimpleJavaCardDLOptions() {
049: public boolean unwindLoops() {
050: return true;
051: }
052:
053: public Name name() {
054: return new Name(BASE_NAME
055: + " without expanding method bodies");
056: }
057: };
058:
059: public static final SimpleJavaCardDLOptions GAMMA_LOOPS_METHODS = new SimpleJavaCardDLOptions() {
060: public boolean test() {
061: return true;
062: }
063:
064: public boolean unwindLoops() {
065: return true;
066: }
067:
068: public boolean expandMethods() {
069: return true;
070: }
071:
072: public Name name() {
073: return new Name(BASE_NAME + " for Unit Test Generation ");
074: }
075: };
076:
077: public static final SimpleJavaCardDLOptions LOOPS_METHODS = new SimpleJavaCardDLOptions() {
078: public boolean unwindLoops() {
079: return true;
080: }
081:
082: public boolean expandMethods() {
083: return true;
084: }
085:
086: public Name name() {
087: return new Name(BASE_NAME);
088: }
089: };
090:
091: public static final SimpleJavaCardDLOptions METHODS = new SimpleJavaCardDLOptions() {
092: public boolean expandMethods() {
093: return true;
094: }
095:
096: public Name name() {
097: return new Name(BASE_NAME + " without unwinding loops");
098: }
099: };
100:
101: public static final SimpleJavaCardDLOptions CONTRACTS = new SimpleJavaCardDLOptions() {
102: public boolean useMethodContracts() {
103: return true;
104: }
105:
106: public Name name() {
107: return new Name(BASE_NAME
108: + " Using Method Contracts without "
109: + "expanding loops and method bodies");
110: }
111: };
112:
113: public static final SimpleJavaCardDLOptions CONTRACTS_LOOPS = new SimpleJavaCardDLOptions() {
114: public boolean unwindLoops() {
115: return true;
116: }
117:
118: public boolean useMethodContracts() {
119: return true;
120: }
121:
122: public Name name() {
123: return new Name(BASE_NAME
124: + " Using Method Contracts without "
125: + "expanding method bodies");
126: }
127: };
128:
129: public static final SimpleJavaCardDLOptions CONTRACTS_METHODS = new SimpleJavaCardDLOptions() {
130: public boolean expandMethods() {
131: return true;
132: }
133:
134: public boolean useMethodContracts() {
135: return true;
136: }
137:
138: public Name name() {
139: return new Name(BASE_NAME
140: + " Using Method Contracts without "
141: + "unwinding loops");
142: }
143: };
144:
145: public static final SimpleJavaCardDLOptions CONTRACTS_LOOPS_METHODS = new SimpleJavaCardDLOptions() {
146: public boolean expandMethods() {
147: return true;
148: }
149:
150: public boolean useMethodContracts() {
151: return true;
152: }
153:
154: public boolean unwindLoops() {
155: return true;
156: }
157:
158: public Name name() {
159: return new Name(BASE_NAME + " Using Method Contracts");
160: }
161: };
162:
163: }
|