Source Code Cross Referenced for RuleAppIndex.java in  » Testing » KeY » de » uka » ilkd » key » proof » 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.proof 
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.proof;
012:
013:        import java.util.ArrayList;
014:        import java.util.Collections;
015:        import java.util.Iterator;
016:        import java.util.List;
017:
018:        import de.uka.ilkd.key.java.Services;
019:        import de.uka.ilkd.key.logic.Constraint;
020:        import de.uka.ilkd.key.logic.PosInOccurrence;
021:        import de.uka.ilkd.key.logic.SequentChangeInfo;
022:        import de.uka.ilkd.key.rule.*;
023:
024:        /**
025:         * manages the possible application of rules (RuleApps) 
026:         */
027:        public class RuleAppIndex {
028:
029:            private Goal goal;
030:
031:            private TacletIndex tacletIndex;
032:
033:            /**
034:             * Two <code>TacletAppIndex</code> objects, one of which only contains rules
035:             * that have to be applied interactively, and the other one for rules that
036:             * can also be applied automatic. This is used as an optimization, as only
037:             * the latter index has to be kept up to date while applying rules automated
038:             */
039:            private TacletAppIndex interactiveTacletAppIndex;
040:            private TacletAppIndex automatedTacletAppIndex;
041:
042:            private BuiltInRuleAppIndex builtInRuleAppIndex;
043:
044:            private List listenerList = Collections
045:                    .synchronizedList(new ArrayList(10));
046:
047:            /**
048:             * The current mode of the index: For <code>autoMode==true</code>, the index
049:             * <code>interactiveTacletAppIndex</code> is not updated
050:             */
051:            private boolean autoMode;
052:
053:            public RuleAppIndex(TacletAppIndex p_tacletAppIndex,
054:                    BuiltInRuleAppIndex p_builtInRuleAppIndex) {
055:                this (p_tacletAppIndex.tacletIndex(), p_builtInRuleAppIndex);
056:            }
057:
058:            public RuleAppIndex(TacletIndex p_tacletIndex,
059:                    BuiltInRuleAppIndex p_builtInRuleAppIndex) {
060:                tacletIndex = p_tacletIndex;
061:                automatedTacletAppIndex = new TacletAppIndex(tacletIndex);
062:                interactiveTacletAppIndex = new TacletAppIndex(tacletIndex);
063:                builtInRuleAppIndex = p_builtInRuleAppIndex;
064:                // default to false to keep compatibility with old code
065:                autoMode = false;
066:
067:                automatedTacletAppIndex
068:                        .setRuleFilter(AnyRuleSetTacletFilter.INSTANCE);
069:                interactiveTacletAppIndex.setRuleFilter(new NotRuleFilter(
070:                        AnyRuleSetTacletFilter.INSTANCE));
071:
072:                setNewRuleListeners();
073:            }
074:
075:            private RuleAppIndex(TacletIndex tacletIndex,
076:                    TacletAppIndex interactiveTacletAppIndex,
077:                    TacletAppIndex automatedTacletAppIndex,
078:                    BuiltInRuleAppIndex builtInRuleAppIndex, boolean autoMode) {
079:                this .tacletIndex = tacletIndex;
080:                this .interactiveTacletAppIndex = interactiveTacletAppIndex;
081:                this .automatedTacletAppIndex = automatedTacletAppIndex;
082:                this .builtInRuleAppIndex = builtInRuleAppIndex;
083:                this .autoMode = autoMode;
084:
085:                setNewRuleListeners();
086:            }
087:
088:            private void setNewRuleListeners() {
089:                NewRuleListener newRuleListener = new NewRuleListener() {
090:                    public void ruleAdded(RuleApp taclet, PosInOccurrence pos) {
091:                        informNewRuleListener(taclet, pos);
092:                    }
093:                };
094:                interactiveTacletAppIndex.setNewRuleListener(newRuleListener);
095:                automatedTacletAppIndex.setNewRuleListener(newRuleListener);
096:                builtInRuleAppIndex.setNewRuleListener(newRuleListener);
097:            }
098:
099:            public void setup(Goal p_goal) {
100:                goal = p_goal;
101:                interactiveTacletAppIndex.setup(p_goal);
102:                automatedTacletAppIndex.setup(p_goal);
103:            }
104:
105:            /**
106:             * Currently the rule app index can either operate in interactive mode (and
107:             * contain applications of all existing taclets) or in automatic mode (and
108:             * only contain a restricted set of taclets that can possibly be applied
109:             * automated). This distinction could be replaced with a more general way to
110:             * control the contents of the rule app index
111:             */
112:            public void autoModeStarted() {
113:                autoMode = true;
114:            }
115:
116:            public void autoModeStopped() {
117:                autoMode = false;
118:            }
119:
120:            /**
121:             * returns the Taclet index for this ruleAppIndex. 
122:             */
123:            public TacletIndex tacletIndex() {
124:                return tacletIndex;
125:            }
126:
127:            /**
128:             * returns the built-in rule application index for this
129:             * ruleAppIndex. 
130:             */
131:            public BuiltInRuleAppIndex builtInRuleAppIndex() {
132:                return builtInRuleAppIndex;
133:            }
134:
135:            /**
136:             * adds a change listener to the index
137:             * @param l the AppIndexListener to add
138:             */
139:            public void addNewRuleListener(NewRuleListener l) {
140:                listenerList.add(l);
141:            }
142:
143:            /**
144:             * removes a change listener to the index
145:             * @param l the AppIndexListener to remove
146:             */
147:            public void removeNewRuleListener(NewRuleListener l) {
148:                listenerList.remove(l);
149:            }
150:
151:            /**returns the set of rule applications for
152:             * the given heuristics 
153:             * at the given position of the given sequent.
154:             * @param filter the TacletFiler filtering the taclets of interest
155:             * @param pos the PosInOccurrence to focus
156:             * @param services the Services object encapsulating information
157:             * about the java datastructures like (static)types etc.
158:             * @param userConstraint the Constraint with user defined instantiations
159:             * of meta variables
160:             */
161:            public ListOfTacletApp getTacletAppAt(TacletFilter filter,
162:                    PosInOccurrence pos, Services services,
163:                    Constraint userConstraint) {
164:                ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
165:                if (!autoMode) {
166:                    result = result.prepend(interactiveTacletAppIndex
167:                            .getTacletAppAt(pos, filter, services,
168:                                    userConstraint));
169:                }
170:                result = result.prepend(automatedTacletAppIndex.getTacletAppAt(
171:                        pos, filter, services, userConstraint));
172:                return result;
173:            }
174:
175:            /**
176:             * returns the rule applications at the given PosInOccurrence and at all
177:             * Positions below this. The method calls getTacletAppAt for all the
178:             * Positions below.
179:             * @param filter the TacletFiler filtering the taclets of interest
180:             * @param pos the position where to start from
181:             * @param services the Services object encapsulating information
182:             * about the java datastructures like (static)types etc.
183:             * @param userConstraint the Constraint with user defined instantiations
184:             * of meta variables
185:             * @return the possible rule applications 
186:             */
187:            public ListOfTacletApp getTacletAppAtAndBelow(TacletFilter filter,
188:                    PosInOccurrence pos, Services services,
189:                    Constraint userConstraint) {
190:                ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
191:                if (!autoMode) {
192:                    result = result.prepend(interactiveTacletAppIndex
193:                            .getTacletAppAtAndBelow(pos, filter, services,
194:                                    userConstraint));
195:                }
196:                result = result.prepend(automatedTacletAppIndex
197:                        .getTacletAppAtAndBelow(pos, filter, services,
198:                                userConstraint));
199:                return result;
200:            }
201:
202:            /** 
203:             * collects all FindTacletInstantiations for the given
204:             * heuristics and position
205:             * @param filter the TacletFiler filtering the taclets of interest
206:             * @param pos the PosInOccurrence to focus
207:             * @param services the Services object encapsulating information
208:             * about the java datastructures like (static)types etc.
209:             * @param userConstraint the Constraint with user defined instantiations
210:             * of meta variables
211:             * @return list of all possible instantiations
212:             */
213:            public ListOfNoPosTacletApp getFindTaclet(TacletFilter filter,
214:                    PosInOccurrence pos, Services services,
215:                    Constraint userConstraint) {
216:                ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
217:                if (!autoMode) {
218:                    result = result.prepend(interactiveTacletAppIndex
219:                            .getFindTaclet(pos, filter, services,
220:                                    userConstraint));
221:                }
222:                result = result.prepend(automatedTacletAppIndex.getFindTaclet(
223:                        pos, filter, services, userConstraint));
224:                return result;
225:            }
226:
227:            /** 
228:             * collects all NoFindTacletInstantiations for the given
229:             * heuristics 
230:             * @param filter the TacletFiler filtering the taclets of interest
231:             * @param services the Services object encapsulating information
232:             * about the java datastructures like (static)types etc.
233:             * @param userConstraint the Constraint with user defined instantiations
234:             * of meta variables
235:             * @return list of all possible instantiations
236:             */
237:            public ListOfNoPosTacletApp getNoFindTaclet(TacletFilter filter,
238:                    Services services, Constraint userConstraint) {
239:                ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
240:                if (!autoMode) {
241:                    result = result.prepend(interactiveTacletAppIndex
242:                            .getNoFindTaclet(filter, services, userConstraint));
243:                }
244:                result = result.prepend(automatedTacletAppIndex
245:                        .getNoFindTaclet(filter, services, userConstraint));
246:                return result;
247:            }
248:
249:            /** 
250:             * collects all RewriteTacletInstantiations for the given
251:             * heuristics in a subterm of the constraintformula described by a
252:             * PosInOccurrence
253:             * @param filter the TacletFiler filtering the taclets of interest
254:             * @param pos the PosInOccurrence to focus
255:             * @param services the Services object encapsulating information
256:             * about the java datastructures like (static)types etc.
257:             * @param userConstraint the Constraint with user defined instantiations
258:             * of meta variables
259:             * @return list of all possible instantiations
260:             */
261:            public ListOfNoPosTacletApp getRewriteTaclet(TacletFilter filter,
262:                    PosInOccurrence pos, Services services,
263:                    Constraint userConstraint) {
264:                ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
265:                if (!autoMode) {
266:                    result = result.prepend(interactiveTacletAppIndex
267:                            .getRewriteTaclet(pos, filter, services,
268:                                    userConstraint));
269:                }
270:                result = result
271:                        .prepend(automatedTacletAppIndex.getRewriteTaclet(pos,
272:                                filter, services, userConstraint));
273:                return result;
274:            }
275:
276:            /** 
277:             * returns a list of built-in rule applications applicable
278:             * for the given goal, user defined constraint and position
279:             */
280:            public ListOfRuleApp getBuiltInRule(Goal goal, PosInOccurrence pos,
281:                    Constraint userConstraint) {
282:
283:                return builtInRuleAppIndex().getBuiltInRule(goal, pos,
284:                        userConstraint);
285:            }
286:
287:            /**
288:             * adds a new Taclet with instantiation information to the Taclet Index 
289:             * of this TacletAppIndex.
290:             * @param tacletApp the NoPosTacletApp describing a partial instantiated Taclet to add
291:             */
292:            public void addNoPosTacletApp(NoPosTacletApp tacletApp) {
293:                tacletIndex.add(tacletApp);
294:
295:                if (autoMode)
296:                    interactiveTacletAppIndex.clearIndexes();
297:
298:                interactiveTacletAppIndex.addedNoPosTacletApp(tacletApp);
299:                automatedTacletAppIndex.addedNoPosTacletApp(tacletApp);
300:            }
301:
302:            /**
303:             * remove a Taclet with instantiation information from the Taclet
304:             * Index of this TacletAppIndex.
305:             * @param tacletApp the NoPosTacletApp to remove
306:             */
307:            public void removeNoPosTacletApp(NoPosTacletApp tacletApp) {
308:                tacletIndex.remove(tacletApp);
309:
310:                if (autoMode)
311:                    interactiveTacletAppIndex.clearIndexes();
312:
313:                interactiveTacletAppIndex.removedNoPosTacletApp(tacletApp);
314:                automatedTacletAppIndex.removedNoPosTacletApp(tacletApp);
315:            }
316:
317:            /** 
318:             * called if a formula has been replaced
319:             * @param goal the Goal which sequent has been changed
320:             * @param sci SequentChangeInfo describing the change of the sequent 
321:             */
322:            public void sequentChanged(Goal goal, SequentChangeInfo sci) {
323:                if (!autoMode)
324:                    // the TacletAppIndex is able to detect modification of the
325:                    // sequent itself, it is not necessary to clear the index
326:                    interactiveTacletAppIndex.sequentChanged(goal, sci);
327:                automatedTacletAppIndex.sequentChanged(goal, sci);
328:                builtInRuleAppIndex().sequentChanged(goal, sci);
329:            }
330:
331:            /**
332:             * Empties all caches
333:             */
334:            public void clearAndDetachCache() {
335:                // Currently this only applies to the taclet index
336:                interactiveTacletAppIndex.clearAndDetachCache();
337:                automatedTacletAppIndex.clearAndDetachCache();
338:            }
339:
340:            /**
341:             * Empties all caches
342:             */
343:            public void clearIndexes() {
344:                // Currently this only applies to the taclet index
345:                interactiveTacletAppIndex.clearIndexes();
346:                automatedTacletAppIndex.clearIndexes();
347:            }
348:
349:            /**
350:             * Ensures that all caches are fully up-to-date
351:             */
352:            public void fillCache() {
353:                if (!autoMode)
354:                    interactiveTacletAppIndex.fillCache();
355:                automatedTacletAppIndex.fillCache();
356:            }
357:
358:            /**
359:             * Report all rule applications that are supposed to be applied
360:             * automatically, and that are currently stored by the index
361:             * 
362:             * @param l the NewRuleListener 
363:             * @param services the Services
364:             * @param userConstraint the Constraint capturing user defined instantiations
365:             * of meta variables
366:             */
367:            public void reportAutomatedRuleApps(NewRuleListener l,
368:                    Services services, Constraint userConstraint) {
369:                automatedTacletAppIndex.reportRuleApps(l, services,
370:                        userConstraint);
371:                builtInRuleAppIndex().reportRuleApps(l, goal, userConstraint);
372:            }
373:
374:            /**
375:             * Report builtin rules to all registered NewRuleListener instances.
376:             * @param p_goal the Goal which to scan
377:             * @param p_userConstraint the Constraint capturing user defined instantiations
378:             * of meta variables 
379:             */
380:            public void scanBuiltInRules(Goal p_goal,
381:                    Constraint p_userConstraint) {
382:                builtInRuleAppIndex().scanApplicableRules(p_goal,
383:                        p_userConstraint);
384:            }
385:
386:            /** 
387:             * informs all observers, if a formula has been added, changed or 
388:             * removed
389:             */
390:            private void informNewRuleListener(RuleApp p_app,
391:                    PosInOccurrence p_pos) {
392:                Iterator it = listenerList.iterator();
393:                while (it.hasNext())
394:                    ((NewRuleListener) it.next()).ruleAdded(p_app, p_pos);
395:            }
396:
397:            /**
398:             * returns a new RuleAppIndex with a copied TacletIndex.
399:             * Attention: the listener lists are not copied
400:             */
401:            public RuleAppIndex copy() {
402:                TacletIndex copiedTacletIndex = tacletIndex.copy();
403:                TacletAppIndex copiedInteractiveTacletAppIndex = interactiveTacletAppIndex
404:                        .copyWithTacletIndex(copiedTacletIndex);
405:                TacletAppIndex copiedAutomatedTacletAppIndex = automatedTacletAppIndex
406:                        .copyWithTacletIndex(copiedTacletIndex);
407:                return new RuleAppIndex(copiedTacletIndex,
408:                        copiedInteractiveTacletAppIndex,
409:                        copiedAutomatedTacletAppIndex, builtInRuleAppIndex()
410:                                .copy(), autoMode);
411:            }
412:
413:            public String toString() {
414:                return "RuleAppIndex with indexing, getting Taclets from"
415:                        + " TacletAppIndex " + interactiveTacletAppIndex
416:                        + " and " + automatedTacletAppIndex;
417:            }
418:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.