Source Code Cross Referenced for TreeAnalyser.java in  » Testing » KeY » de » uka » ilkd » key » ocl » gf » 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.ocl.gf 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


001:        //Copyright (c) Hans-Joachim Daniels 2005
002:
003:        //This program is free software; you can redistribute it and/or modify
004:        //it under the terms of the GNU General Public License as published by
005:        //the Free Software Foundation; either version 2 of the License, or
006:        //(at your option) any later version.
007:
008:        //This program is distributed in the hope that it will be useful,
009:        //but WITHOUT ANY WARRANTY; without even the implied warranty of
010:        //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
011:        //GNU General Public License for more details.
012:
013:        //You can either finde the file LICENSE or LICENSE.TXT in the source 
014:        //distribution or in the .jar file of this application
015:
016:        package de.uka.ilkd.key.ocl.gf;
017:
018:        import java.util.Enumeration;
019:        import java.util.logging.Level;
020:        import java.util.logging.Logger;
021:
022:        import javax.swing.tree.DefaultMutableTreeNode;
023:
024:        /**
025:         * Goes through the AST and:
026:         *   Labels node according to the following:
027:         *     hidden, if they are a coerce without a constraint
028:         *     colored, if they are a coerce with a constraint
029:         *   Saves a reference to the currently selected node
030:         *   Finds out 
031:         *     if attributes of self should be given an easy access,
032:         *     if the refinement menu below a coerce should be reduces,
033:         *     if it should be probed, if self and result are superfluous
034:         *       in the refinement menu.
035:         *     if a coerce should be introduced automatically.
036:         * Takes a tree and hides the nodes labelled as hidden in another stage.
037:         * @author hdaniels
038:         */
039:        class TreeAnalyser {
040:            /** 
041:             * debug stuff for the tree 
042:             */
043:            private static Logger treeLogger = Logger
044:                    .getLogger(TreeAnalyser.class.getName());
045:            /** 
046:             * dealing with coerce, when it is inserted and so on 
047:             */
048:            private static Logger coerceLogger = Logger
049:                    .getLogger(TreeAnalyser.class.getName() + ".coerce");
050:
051:            /**
052:             * if coerce should get hidden, if all their arguments are refined
053:             */
054:            private boolean hideCoerce;
055:            /**
056:             * if coerce should always be hidden,
057:             */
058:            private boolean hideCoerceAggressive;
059:            /**
060:             *  if the refinement menu should get condensed at all
061:             */
062:            private boolean coerceReduceRM;
063:            /**
064:             * if coerce should get introduced automatically at all
065:             */
066:            private boolean autoCoerce;
067:            /**
068:             * if result and self should be shown always
069:             */
070:            private boolean showSelfResult;
071:            /**
072:             * if properties of self should be probed for
073:             */
074:            private boolean easyAttributes;
075:            /**
076:             * If coerces whith both Class arguments
077:             */
078:            private boolean highlightSubtypingErrors;
079:
080:            /**
081:             * @param autoCoerce if coerce should get introduced automatically at all
082:             * @param coerceReduceRM if the refinement menu should get condensed at all
083:             * @param easyAttributes if properties of self should be probed for
084:             * @param hideCoerce if coerce should get hidden, if all their arguments are refined
085:             * @param hideCoerceAggressive if coerce should always be hidden, 
086:             * unless there is a GF constraint
087:             * @param highlightSubtypingErrors If coerces whith both Class arguments 
088:             * refined, but not with the Subtype argument should get marked
089:             * @param showSelfResult if result and self should be shown always
090:             */
091:            public TreeAnalyser(boolean autoCoerce, boolean coerceReduceRM,
092:                    boolean easyAttributes, boolean hideCoerce,
093:                    boolean hideCoerceAggressive,
094:                    boolean highlightSubtypingErrors, boolean showSelfResult) {
095:                this .autoCoerce = autoCoerce;
096:                this .coerceReduceRM = coerceReduceRM;
097:                this .easyAttributes = easyAttributes;
098:                this .hideCoerce = hideCoerce;
099:                this .hideCoerceAggressive = hideCoerceAggressive;
100:                this .highlightSubtypingErrors = highlightSubtypingErrors;
101:                this .showSelfResult = showSelfResult;
102:            }
103:
104:            /**
105:             * Takes the rootNode of the AST and does some small analysis on it:
106:             *   Check for missing Subtype witnesses, 
107:             *   check if the Instance menu of a Coerce can be reduced
108:             * @param topNode The root or top node of the AST
109:             * @return an object that contains the result of this analysis.
110:             * Currently this applies only to the selected node. 
111:             * @see TreeAnalysisResult 
112:             */
113:            TreeAnalysisResult analyseTree(DefaultMutableTreeNode topNode) {
114:                //just the initial values
115:                String resultCommand = null;
116:                int resultUndoSteps = -1;
117:                boolean resultReduceCoerce = false;
118:                boolean resultProbeSelfResult = false;
119:                boolean resultDeleteAlsoAbove = false;
120:                boolean resultEasyAttributes = false;
121:                TreeAnalysisResult tar = new TreeAnalysisResult(resultCommand,
122:                        resultUndoSteps, resultReduceCoerce,
123:                        resultProbeSelfResult, resultDeleteAlsoAbove,
124:                        resultEasyAttributes, null, null);
125:
126:                //doing it depth first, because we have to know the subtypingStatus
127:                //of the children of coerce before we analyze coerce itself
128:                for (Enumeration e = topNode.depthFirstEnumeration(); e
129:                        .hasMoreElements();) {
130:                    DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
131:                            .nextElement();
132:                    analyseTreeNode(currNode, tar);
133:                }
134:                AstNodeData and = (AstNodeData) tar.selectedNode
135:                        .getUserObject();
136:                if ((and.showInstead != -1) && (tar.command == null)) {
137:                    //if the current node is hidden, move up in the tree,
138:                    //until a visible node is found
139:                    DefaultMutableTreeNode tn = (DefaultMutableTreeNode) tar.selectedNode
140:                            .getParent();
141:                    AstNodeData dand = null;
142:                    while (tn != null) {
143:                        dand = (AstNodeData) tn.getUserObject();
144:                        if (dand.showInstead == -1) {
145:                            //found a visible node
146:                            break;
147:                        }
148:                        tn = (DefaultMutableTreeNode) tn.getParent();
149:                    }
150:                    if (dand != null) {
151:                        tar.command = "[tr] mp " + dand.position;
152:                        tar.undoSteps = 1;
153:                    } //otherwise give up, can only occur, if coerce is the top node.
154:                    //And for that, one would have to do a "n Instance" first,
155:                    //which GF does not even offer.
156:                }
157:                return tar;
158:            }
159:
160:            /**
161:             * Takes the rootNode of the AST and does some small analysis on it:
162:             *   Check for missing Subtype witnesses, 
163:             *   check if the Instance menu of a Coerce can be reduced
164:             * @param nodeToCheck The node that is to be analysed
165:             * @param tar The result, that gets modified
166:             * @see TreeAnalysisResult
167:             */
168:            private void analyseTreeNode(DefaultMutableTreeNode nodeToCheck,
169:                    TreeAnalysisResult tar) {
170:                AstNodeData and = (AstNodeData) nodeToCheck.getUserObject();
171:                DefaultMutableTreeNode parent = (DefaultMutableTreeNode) nodeToCheck
172:                        .getParent();
173:                Printname parentPrintname = null;
174:                if ((parent != null) && (parent.getUserObject() != null)
175:                        && (parent.getUserObject() instanceof  AstNodeData)) {
176:                    AstNodeData parentAnd = (AstNodeData) parent
177:                            .getUserObject();
178:                    parentPrintname = parentAnd.getPrintname();
179:                }
180:
181:                if (and.selected) {
182:                    tar.selectedNode = nodeToCheck;
183:                    tar.currentNode = and.node;
184:                    //set the focusPosition to a preliminary value
185:                    tar.focusPosition = new LinPosition(and.position, true);
186:                    //rather check too much for null
187:                    if (this .autoCoerce && (and.node != null)
188:                            && and.node.isMeta() && (parent != null)
189:                            && (parent.getUserObject() != null)
190:                            && (and.node.getType() != null)
191:                            && (and.node.getType().startsWith("Instance"))) {
192:                        //check, if a coerce is needed                                
193:                        GfAstNode parentNode = ((AstNodeData) parent
194:                                .getUserObject()).node;
195:                        if (parentPrintname.getParamAutoCoerce(parent
196:                                .getIndex(nodeToCheck))) {
197:                            coerceLogger.fine("Coerceable fun found: "
198:                                    + and.node + " + " + parentNode);
199:                            //refine with coerce. Do not allow another GF run, so [r]
200:                            tar.command = "[tr] r core.coerce ;; mp "
201:                                    + LinPosition.calculateChildPosition(
202:                                            and.position, 3);
203:                            tar.undoSteps = 2; //move there is also sth. to be undone
204:                        } else if ((parentNode.getFun().indexOf("coerce") > -1)
205:                                //to avoid getting stuck below a coerce with wrong type arguments
206:                                //the coerce above is deleted and rerefined.
207:
208:                                //coerce below a coerce is never done automatically, so the else if is justified,
209:                                //meaning, that introduced a coerce, we do not have to delete it right a away 
210:                                && parent.getParent() != null
211:                                && (parent.getParent() instanceof  DefaultMutableTreeNode)) {
212:                            DefaultMutableTreeNode grandParent = (DefaultMutableTreeNode) parent
213:                                    .getParent();
214:                            if (grandParent != null) {
215:                                AstNodeData grandParentAnd = (AstNodeData) grandParent
216:                                        .getUserObject();
217:                                Printname grandParentPrintname = grandParentAnd
218:                                        .getPrintname();
219:
220:                                if (grandParentPrintname
221:                                        .getParamAutoCoerce(grandParent
222:                                                .getIndex(parent))) {
223:                                    coerceLogger
224:                                            .fine("Auto-Coerce to be un- and redone: "
225:                                                    + and.node
226:                                                    + " + "
227:                                                    + parentNode
228:                                                    + " -- "
229:                                                    + tar.focusPosition.position);
230:                                    tar.command = "[tr] mp "
231:                                            + tar.focusPosition
232:                                                    .parentPosition()
233:                                            + " ;; d ;; mp "
234:                                            + tar.focusPosition
235:                                                    .parentPosition()
236:                                            + " ;; r core.coerce ;; mp "
237:                                            + tar.focusPosition.position;
238:                                    tar.undoSteps = 6;
239:                                }
240:                            }
241:                        }
242:                    }
243:
244:                    if (coerceReduceRM
245:                            && (and.node != null)
246:                            && (and.node.getType() != null)
247:                            && (parent != null)
248:                            && (parent.getUserObject() != null)
249:                            && (((AstNodeData) parent.getUserObject())
250:                                    .getPrintname() != null)
251:                            && (((AstNodeData) parent.getUserObject())
252:                                    .getPrintname().fun.endsWith("coerce"))
253:                            && (and.node.getType().startsWith("Instance")) //if coerce, than we are the Instance argument
254:                            && (((DefaultMutableTreeNode) (parent.getChildAt(2)))
255:                                    .getUserObject() != null)
256:                            && (parent.getChildAt(2) != null)
257:                            && ((AstNodeData) ((DefaultMutableTreeNode) (parent
258:                                    .getChildAt(2))).getUserObject()).node
259:                                    .isMeta()) {
260:                        AstNodeData super TypeAnd = ((AstNodeData) ((DefaultMutableTreeNode) (parent
261:                                .getChildAt(1))).getUserObject());
262:                        if (!super TypeAnd.node.isMeta()
263:                                && (super TypeAnd.node.getFun().indexOf(
264:                                        "OclAnyC") == -1)) {
265:                            //in these cases, everything goes. No sense in dozends of expensive GF runs then.
266:                            tar.reduceCoerce = true;
267:                        }
268:                        coerceLogger
269:                                .fine("candidate for coerce reduction found: "
270:                                        + and.node + " + " + parent);
271:                    }
272:
273:                    if (showSelfResult && (and.node != null)
274:                            && (and.node.getType() != null)
275:                            && (and.node.getType().startsWith("Instance"))
276:                            && (tar.reduceCoerce //not everything is allowed here
277:                            // if not below a coerce (covered above) and no constraints
278:                            || (and.node.getType().indexOf("{") == -1))) {
279:                        //if there are constraints present, there is no point in probing, since
280:                        //then either no or every instance is offered.
281:                        //We do not have to probe then.
282:                        tar.probeSelfResult = true;
283:                    }
284:
285:                    if (easyAttributes && (and.node != null)
286:                            && (and.node.getType() != null)
287:                            && (and.node.isMeta())
288:                            && (and.node.getType().startsWith("Instance"))) {
289:                        //not much to check here
290:                        tar.easyAttributes = true;
291:                    }
292:                }
293:
294:                //check for subtyping errors
295:                if (highlightSubtypingErrors && (and.node != null)
296:                        && (and.node.getType() != null) && (parent != null)
297:                        && (and.node.isMeta()) //otherwise GF would complain
298:                        && (and.node.getType().startsWith("Subtype")) //if coerce, than we are the Subtype argument
299:                ) {
300:                    AstNodeData subtypeAnd = (AstNodeData) (((DefaultMutableTreeNode) (parent
301:                            .getChildAt(0))).getUserObject());
302:                    AstNodeData super typeAnd = (AstNodeData) (((DefaultMutableTreeNode) (parent
303:                            .getChildAt(1))).getUserObject());
304:                    if ((subtypeAnd != null) && (super typeAnd != null)) {
305:                        if (!super typeAnd.node.isMeta()
306:                                && !subtypeAnd.node.isMeta()) {
307:                            //if one of them is meta, then the situation is not fixed yet,
308:                            //so don't complain.
309:                            and.subtypingStatus = false;
310:                        }
311:                    }
312:                }
313:                //hide coerce if possible
314:                //if coere is completely filled in (all children not meta),
315:                //it will be replaced by child 3.
316:                if (hideCoerce && (and.node != null)
317:                        && (and.node.getType() != null)
318:                        && (and.node.getFun().endsWith("coerce"))) {
319:                    /** 
320:                     * if true, then something is unfinished or constrained.
321:                     * So don't hide that node.
322:                     */
323:                    boolean metaChild = false;
324:                    //check if constraints hold for this node
325:                    if ((and.constraint != null)
326:                            && (and.constraint.length() > 0)) {
327:                        //some constraint holds here. 
328:                        //We must not shroud a possible source for that.
329:                        metaChild = true;
330:                    }
331:                    //This search will only be run once for each coerce:
332:                    for (int i = 0; i < 3 && !metaChild; i++) {
333:                        //This is for the more complicated collection
334:                        //subtyping witnesses.
335:                        //we do a depthFirst search to find meta nodes.
336:                        //If they exist, we know that we shouldn't hide this node.
337:                        for (Enumeration e = ((DefaultMutableTreeNode) nodeToCheck
338:                                .getChildAt(i)).depthFirstEnumeration(); e
339:                                .hasMoreElements();) {
340:                            DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
341:                                    .nextElement();
342:                            AstNodeData dand = (AstNodeData) currNode
343:                                    .getUserObject();
344:                            if (!dand.subtypingStatus
345:                            //hideCoerceAggressive means that just incomplete type arguments are no reason to not hide the node
346:                                    //only subtypingStatus is one because then surely there is an error
347:                                    || (!hideCoerceAggressive && dand.node
348:                                            .isMeta())) {
349:                                metaChild = true;
350:                                break; //no need to go further
351:                            }
352:                        }
353:                        if (metaChild) {
354:                            break;
355:                        }
356:                    }
357:                    //For the Instance argument, we do not have do to a deep search 
358:                    AstNodeData childAnd = (AstNodeData) (((DefaultMutableTreeNode) (nodeToCheck
359:                            .getChildAt(3))).getUserObject());
360:                    if (!hideCoerceAggressive && childAnd.node.isMeta()) {
361:                        //see reasons for hideCoerceAggressive above
362:                        metaChild = true;
363:                    }
364:
365:                    if (!metaChild) {
366:                        and.showInstead = 3;
367:                        //now label the type nodes as hidden
368:                        for (int i = 0; i < 3 && !metaChild; i++) {
369:                            //This is for the more complicated collection
370:                            //subtyping witnesses.
371:                            for (Enumeration e = ((DefaultMutableTreeNode) nodeToCheck
372:                                    .getChildAt(i)).depthFirstEnumeration(); e
373:                                    .hasMoreElements();) {
374:                                DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
375:                                        .nextElement();
376:                                AstNodeData dand = (AstNodeData) currNode
377:                                        .getUserObject();
378:                                dand.showInstead = -2; // tag for hidden without replacement
379:                            }
380:                        }
381:
382:                    }
383:
384:                    //if we are at a coerce above the selected Instance node,
385:                    //we want to mark that, so that the d command can be modified
386:                    if ((and.node != null)
387:                            && (and.node.getFun().endsWith("coerce"))
388:                            && (and.showInstead > -1) //only hidden coerce
389:                            && (((AstNodeData) ((DefaultMutableTreeNode) nodeToCheck
390:                                    .getChildAt(3)).getUserObject()).selected)) {
391:                        tar.deleteAlsoAbove = true;
392:                    }
393:                }
394:            }
395:
396:            /**
397:             * Removes nodes from the tree that has topNode as its root.
398:             * Affected are nodes in which the field showInstead in their
399:             * AstNodeData is greater than -1
400:             * @param topNode The root of the tree from which nodes should
401:             * be removed.
402:             * @return The root of the transformed tree. 
403:             * This might not be topNode, since that node might as well be 
404:             * removed. 
405:             */
406:            protected static DefaultMutableTreeNode transformTree(
407:                    DefaultMutableTreeNode topNode) {
408:                DefaultMutableTreeNode nextNode = topNode;
409:                while (nextNode != null) {
410:                    AstNodeData and = (AstNodeData) nextNode.getUserObject();
411:                    if (and.showInstead > -1) {
412:                        DefaultMutableTreeNode parent = (DefaultMutableTreeNode) nextNode
413:                                .getParent();
414:                        if (parent == null) {
415:                            topNode = (DefaultMutableTreeNode) nextNode
416:                                    .getChildAt(and.showInstead);
417:                            if (treeLogger.isLoggable(Level.FINE)) {
418:                                //yeah, I know, variable naming is messed up here because of the assignment above
419:                                treeLogger.fine("hiding topNode ###" + nextNode
420:                                        + "###, showing instead ###" + topNode
421:                                        + "###");
422:                            }
423:                            nextNode = topNode;
424:                        } else {
425:                            final int index = parent.getIndex(nextNode);
426:                            parent.remove(index);
427:                            DefaultMutableTreeNode instead = (DefaultMutableTreeNode) nextNode
428:                                    .getChildAt(and.showInstead);
429:                            parent.insert(instead, index);
430:                            if (treeLogger.isLoggable(Level.FINE)) {
431:                                treeLogger.fine("hiding node ###" + nextNode
432:                                        + "###, showing instead ###" + instead
433:                                        + "###");
434:                            }
435:                            nextNode = instead;
436:                        }
437:                    } else {
438:                        nextNode = nextNode.getNextNode();
439:                    }
440:                }
441:                return topNode;
442:            }
443:
444:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.