Source Code Cross Referenced for ShannonFeature.java in  » Testing » KeY » de » uka » ilkd » key » strategy » feature » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.strategy.feature 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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.feature;
012:
013:        import de.uka.ilkd.key.logic.PosInOccurrence;
014:        import de.uka.ilkd.key.proof.Goal;
015:        import de.uka.ilkd.key.rule.RuleApp;
016:        import de.uka.ilkd.key.strategy.LongRuleAppCost;
017:        import de.uka.ilkd.key.strategy.RuleAppCost;
018:
019:        /**
020:         * A conditional feature, in which the condition itself is a (binary) feature.
021:         * The general notion is a term <code>c ? f1 : f2</code>, whereby the
022:         * condition <code>c</code> determines whether the value of the whole
023:         * expression is <code>f1</code> (if <code>c</code> returns zero, or more
024:         * general if <code>c</code> returns a distinguished value
025:         * <code>trueCost</code>) or <code>f2</code>
026:         */
027:        public class ShannonFeature implements  Feature {
028:
029:            /**
030:             * The filter that decides which sub-feature is to be evaluated
031:             */
032:            private final Feature cond;
033:
034:            /**
035:             * If the result of <code>cond</code> is this cost, then the condition
036:             * is assumed to hold
037:             */
038:            private final RuleAppCost trueCost;
039:
040:            /**
041:             * The feature for positive results of <code>filter</code>
042:             */
043:            private final Feature thenFeature;
044:
045:            /**
046:             * The feature for negative results of <code>filter</code>
047:             */
048:            private final Feature elseFeature;
049:
050:            private ShannonFeature(Feature p_cond, RuleAppCost p_trueCost,
051:                    Feature p_thenFeature, Feature p_elseFeature) {
052:                cond = p_cond;
053:                trueCost = p_trueCost;
054:                thenFeature = p_thenFeature;
055:                elseFeature = p_elseFeature;
056:            }
057:
058:            public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
059:                    Goal goal) {
060:                if (cond.compute(app, pos, goal).equals(trueCost))
061:                    return thenFeature.compute(app, pos, goal);
062:                else
063:                    return elseFeature.compute(app, pos, goal);
064:            }
065:
066:            /**
067:             * @param cond
068:             *            the feature that decides which value is to be returned
069:             * @param trueCost
070:             *            the value of <code>cond</code> that is regarded as
071:             *            true-value
072:             * @param thenValue
073:             *            the value of the feature, if <code>cond</code> returns
074:             *            <code>trueCost</code>
075:             * @return <code>thenValue</code> if <code>cond</code> returns
076:             *         <code>trueCost</code>, zero otherwise
077:             */
078:            public static Feature createConditional(Feature cond,
079:                    RuleAppCost trueCost, RuleAppCost thenValue) {
080:                return createConditional(cond, trueCost, ConstFeature
081:                        .createConst(thenValue));
082:            }
083:
084:            /**
085:             * @param cond
086:             *            the feature that decides which value is to be returned
087:             * @param trueCost
088:             *            the value of <code>cond</code> that is regarded as
089:             *            true-value
090:             * @param thenValue
091:             *            the value of the feature if <code>cond</code> returns
092:             *            <code>trueCost</code>
093:             * @param elseValue
094:             *            the value of the feature if <code>cond</code> does not
095:             *            return <code>trueCost</code>
096:             * @return <code>thenValue</code> if <code>cond</code> returns
097:             *         <code>trueCost</code>, <code>elseValue</code> otherwise
098:             */
099:            public static Feature createConditional(Feature cond,
100:                    RuleAppCost trueCost, RuleAppCost thenValue,
101:                    RuleAppCost elseValue) {
102:                return createConditional(cond, trueCost, ConstFeature
103:                        .createConst(thenValue), ConstFeature
104:                        .createConst(elseValue));
105:            }
106:
107:            /**
108:             * @param cond
109:             *            the feature that decides which value is to be returned
110:             * @param trueCost
111:             *            the value of <code>cond</code> that is regarded as
112:             *            true-value
113:             * @param thenFeature
114:             *            the value of the feature if <code>cond</code> returns
115:             *            <code>trueCost</code>
116:             * @return the value of <code>thenFeature</code> if <code>cond</code>
117:             *         returns <code>trueCost</code>, zero otherwise
118:             */
119:            public static Feature createConditional(Feature cond,
120:                    RuleAppCost trueCost, Feature thenFeature) {
121:                return createConditional(cond, trueCost, thenFeature,
122:                        LongRuleAppCost.ZERO_COST);
123:            }
124:
125:            /**
126:             * @param cond
127:             *            the feature that decides which value is to be returned
128:             * @param trueCost
129:             *            the value of <code>cond</code> that is regarded as
130:             *            true-value
131:             * @param thenFeature
132:             *            the value of the feature if <code>cond</code> returns
133:             *            <code>trueCost</code>
134:             * @param elseValue
135:             *            the value of the feature if <code>cond</code> does not
136:             *            return <code>trueCost</code>
137:             * @return the value of <code>thenFeature</code> if <code>cond</code>
138:             *         returns <code>trueCost</code>, <code>elseValue</code>
139:             *         otherwise
140:             */
141:            public static Feature createConditional(Feature cond,
142:                    RuleAppCost trueCost, Feature thenFeature,
143:                    RuleAppCost elseValue) {
144:                return createConditional(cond, trueCost, thenFeature,
145:                        ConstFeature.createConst(elseValue));
146:            }
147:
148:            /**
149:             * @param cond
150:             *            the feature that decides which value is to be returned
151:             * @param trueCost
152:             *            the value of <code>cond</code> that is regarded as
153:             *            true-value
154:             * @param thenFeature
155:             *            the value of the feature if <code>cond</code> returns
156:             *            <code>trueCost</code>
157:             * @param elseFeature
158:             *            the value of the feature if <code>cond</code> does not
159:             *            return <code>trueCost</code>
160:             * @return the value of <code>thenFeature</code> if <code>cond</code>
161:             *         returns <code>trueCost</code>, the value of
162:             *         <code>elseFeature</code> otherwise
163:             */
164:            public static Feature createConditional(Feature cond,
165:                    RuleAppCost trueCost, Feature thenFeature,
166:                    Feature elseFeature) {
167:                return new ShannonFeature(cond, trueCost, thenFeature,
168:                        elseFeature);
169:            }
170:
171:            /**
172:             * @param cond
173:             *            the feature that decides which value is to be returned
174:             * @param thenValue
175:             *            the value of the feature if <code>cond</code> returns zero
176:             * @return the value of <code>thenFeature</code> if <code>cond</code>
177:             *         returns zero, zero otherwise
178:             */
179:            public static Feature createConditionalBinary(Feature cond,
180:                    RuleAppCost thenValue) {
181:                return createConditionalBinary(cond, ConstFeature
182:                        .createConst(thenValue));
183:            }
184:
185:            /**
186:             * @param cond
187:             *            the feature that decides which value is to be returned
188:             * @param thenValue
189:             *            the value of the feature if <code>cond</code> returns zero
190:             * @param elseValue
191:             *            the value of the feature if <code>cond</code> does not
192:             *            return zero
193:             * @return <code>thenValue</code> if <code>cond</code> returns zero,
194:             *         <code>elseValue</code> otherwise
195:             */
196:            public static Feature createConditionalBinary(Feature cond,
197:                    RuleAppCost thenValue, RuleAppCost elseValue) {
198:                return createConditionalBinary(cond, ConstFeature
199:                        .createConst(thenValue), ConstFeature
200:                        .createConst(elseValue));
201:            }
202:
203:            /**
204:             * @param cond
205:             *            the feature that decides which value is to be returned
206:             * @param thenFeature
207:             *            the value of the feature if <code>cond</code> returns zero
208:             * @param elseValue
209:             *            the value of the feature if <code>cond</code> does not
210:             *            return zero
211:             * @return the value of <code>thenFeature</code> if <code>cond</code>
212:             *         returns zero, <code>elseValue</code> otherwise
213:             */
214:            public static Feature createConditionalBinary(Feature cond,
215:                    Feature thenFeature, RuleAppCost elseValue) {
216:                return createConditionalBinary(cond, thenFeature, ConstFeature
217:                        .createConst(elseValue));
218:            }
219:
220:            /**
221:             * @param cond
222:             *            the feature that decides which value is to be returned
223:             * @param thenFeature
224:             *            the value of the feature if <code>cond</code> returns zero
225:             * @param elseFeature
226:             *            the value of the feature if <code>cond</code> does not
227:             *            return zero
228:             * @return the value of <code>thenFeature</code> if <code>cond</code>
229:             *         returns zero, the value of <code>elseFeature</code> otherwise
230:             */
231:            public static Feature createConditionalBinary(Feature cond,
232:                    Feature thenFeature, Feature elseFeature) {
233:                return createConditional(cond, BinaryFeature.ZERO_COST,
234:                        thenFeature, elseFeature);
235:            }
236:
237:            /**
238:             * @param cond
239:             *            the feature that decides which value is to be returned
240:             * @param thenFeature
241:             *            the value of the feature if <code>cond</code> returns zero
242:             * @return the value of <code>thenFeature</code> if <code>cond</code>
243:             *         returns zero, zero otherwise
244:             */
245:            public static Feature createConditionalBinary(Feature cond,
246:                    Feature thenFeature) {
247:                return createConditional(cond, BinaryFeature.ZERO_COST,
248:                        thenFeature, LongRuleAppCost.ZERO_COST);
249:            }
250:
251:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.