Source Code Cross Referenced for Node.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.*;
014:
015:        import de.uka.ilkd.key.logic.Constraint;
016:        import de.uka.ilkd.key.logic.ListOfRenamingTable;
017:        import de.uka.ilkd.key.logic.Sequent;
018:        import de.uka.ilkd.key.logic.op.*;
019:        import de.uka.ilkd.key.proof.incclosure.*;
020:        import de.uka.ilkd.key.proof.reuse.ReusePoint;
021:        import de.uka.ilkd.key.rule.*;
022:        import de.uka.ilkd.key.util.Debug;
023:
024:        public class Node {
025:            /** the proof the node belongs to */
026:            private Proof proof;
027:
028:            private Sequent seq = Sequent.EMPTY_SEQUENT;
029:
030:            private List children = new LinkedList();
031:
032:            private Node parent = null;
033:
034:            private RuleApp appliedRuleApp;
035:
036:            private SetOfProgramVariable globalProgVars = SetAsListOfProgramVariable.EMPTY_SET;
037:
038:            private boolean closed = false;
039:
040:            /** Root sink if this is a root node */
041:            private BufferSink rootSink = null;
042:
043:            private BufferSink localSink;
044:
045:            /** Parent of all sinks on this branch */
046:            private Sink branchSink;
047:
048:            /** For children.size()>1 this merger will be used */
049:            private MultiMerger forkMerger = null;
050:
051:            /** contains non-logical content, used for user feedback */
052:            private NodeInfo nodeInfo;
053:
054:            int reuseCandidate = 0;
055:
056:            private boolean persistentCandidate = false;
057:
058:            private ReusePoint reuseSource;
059:
060:            int serialNr;
061:
062:            private int siblingNr = -1;
063:
064:            private ListOfRenamingTable renamings;
065:
066:            /**
067:             * If the rule base has been extended e.g. by loading a new taclet as
068:             * lemma or by applying a taclet with an addrule section on this node,
069:             * then these taclets are stored in this set
070:             */
071:            private SetOfNoPosTacletApp localIntroducedRules = SetAsListOfNoPosTacletApp.EMPTY_SET;
072:
073:            /** creates an empty node that is root and leaf.
074:             */
075:            public Node(Proof proof) {
076:                this .proof = proof;
077:                rootSink = new BufferSink(null);
078:                branchSink = new BranchRestricter(rootSink);
079:                ((BranchRestricter) branchSink).setNode(this );
080:                localSink = new BufferSink(branchSink);
081:                serialNr = proof.getServices().getCounter("nodes")
082:                        .getCountPlusPlus(this );
083:                nodeInfo = new NodeInfo(this );
084:            }
085:
086:            /** creates a node with the given contents
087:             */
088:            public Node(Proof proof, Sequent seq) {
089:                this (proof);
090:                this .seq = seq;
091:                serialNr = proof.getServices().getCounter("nodes")
092:                        .getCountPlusPlus(this );
093:            }
094:
095:            /** creates a node with the given contents, the given collection
096:             * of children (all elements must be of class Node) and the given
097:             * parent node.
098:             */
099:            public Node(Proof proof, Sequent seq, List children, Node parent,
100:                    Sink branchSink) {
101:                this .proof = proof;
102:                this .seq = seq;
103:                this .parent = parent;
104:                this .branchSink = branchSink;
105:                localSink = new BufferSink(branchSink);
106:                if (children != null) {
107:                    this .children = children;
108:                }
109:                serialNr = proof.getServices().getCounter("nodes")
110:                        .getCountPlusPlus(this );
111:                nodeInfo = new NodeInfo(this );
112:            }
113:
114:            /** sets the sequent at this node
115:             */
116:            public void setSequent(Sequent seq) {
117:                this .seq = seq;
118:            }
119:
120:            /** returns the sequent of this node */
121:            public Sequent sequent() {
122:                return seq;
123:            }
124:
125:            /**
126:             * the node information object encapsulates non-logical information
127:             * of the node, e.g.  
128:             * 
129:             * @return
130:             */
131:            public NodeInfo getNodeInfo() {
132:                return nodeInfo;
133:            }
134:
135:            /** returns the proof the Node belongs to */
136:            public Proof proof() {
137:                return proof;
138:            }
139:
140:            public void setAppliedRuleApp(RuleApp ruleApp) {
141:                this .appliedRuleApp = ruleApp;
142:            }
143:
144:            public void setRenamings(ListOfRenamingTable list) {
145:                renamings = list;
146:            }
147:
148:            public ListOfRenamingTable getRenamingTable() {
149:                return renamings;
150:            }
151:
152:            public RuleApp getAppliedRuleApp() {
153:                return appliedRuleApp;
154:            }
155:
156:            /** Returns the set of NoPosTacletApps at this node */
157:            public SetOfNoPosTacletApp getNoPosTacletApps() {
158:                return localIntroducedRules;
159:            }
160:
161:            public SetOfProgramVariable getGlobalProgVars() {
162:                return globalProgVars;
163:            }
164:
165:            public void setGlobalProgVars(SetOfProgramVariable progVars) {
166:                globalProgVars = progVars;
167:            }
168:
169:            /**
170:             * adds a new NoPosTacletApp to the set of available NoPosTacletApps 
171:             * at this node
172:             */
173:            public void addNoPosTacletApp(NoPosTacletApp s) {
174:                localIntroducedRules = localIntroducedRules.add(s);
175:            }
176:
177:            /** returns the parent node of this node.
178:             */
179:            public Node parent() {
180:                return parent;
181:            }
182:
183:            /** returns true, iff this node is a leaf, i.e. has no children.
184:             */
185:            public boolean leaf() {
186:                return children.size() == 0;
187:            }
188:
189:            /** searches for a given node in the subtree starting with this node */
190:            public boolean find(Node node) {
191:                // we assume that the proof tree node is part of has proper
192:                // links
193:
194:                while (node != this ) {
195:                    if (node.root())
196:                        return false;
197:                    node = node.parent();
198:                }
199:
200:                return true;
201:            }
202:
203:            /**
204:             * Search for the node being the root of the smallest subtree
205:             * containing <code>this</code> and <code>p_node</code>; we assume
206:             * that the two nodes are part of the same proof tree
207:             */
208:            public Node commonAncestor(Node p_node) {
209:                if (root())
210:                    return this ;
211:                if (p_node.root())
212:                    return p_node;
213:
214:                HashSet paths = new HashSet();
215:                Node n = this ;
216:
217:                while (true) {
218:                    if (!paths.add(n))
219:                        return n;
220:                    if (n.root())
221:                        break;
222:                    n = n.parent();
223:
224:                    if (!paths.add(p_node))
225:                        return p_node;
226:                    if (p_node.root()) {
227:                        p_node = n;
228:                        break;
229:                    }
230:                    p_node = p_node.parent();
231:                }
232:
233:                while (!paths.contains(p_node))
234:                    p_node = p_node.parent();
235:
236:                return p_node;
237:            }
238:
239:            /**  returns true, iff this node is root, i.e. has no parents.
240:             */
241:            public boolean root() {
242:                return parent == null;
243:            }
244:
245:            /**
246:             * Reserve p_count sinks meant for children and return them. If
247:             * ultimately more than one sink is needed, the first call to this
248:             * method MUST have p_count>1.
249:             */
250:            public IteratorOfSink reserveSinks(int p_count) {
251:                if (p_count == 1 && forkMerger == null)
252:                    return SLListOfSink.EMPTY_LIST.prepend(branchSink)
253:                            .iterator();
254:                else {
255:                    int i = 0;
256:
257:                    if (forkMerger == null)
258:                        forkMerger = new MultiMerger(branchSink, p_count, proof
259:                                .getServices());
260:                    else {
261:                        i = forkMerger.getArity();
262:                        forkMerger.expand(i + p_count);
263:                    }
264:
265:                    IteratorOfSink it = forkMerger.getSinks();
266:                    while (i-- != 0)
267:                        it.next();
268:
269:                    return it;
270:                }
271:            }
272:
273:            /**
274:             * Remove a possibly existing merger, restore the old state by
275:             * calling "localSink.reset()". Currently this doesn't really
276:             * remove the connection between the children sinks and the branch
277:             * sink.
278:             */
279:            public void cutChildrenSinks() {
280:                if (forkMerger != null)
281:                    forkMerger = null;
282:
283:                resetBranchSink();
284:            }
285:
286:            /**
287:             * 
288:             */
289:            public void resetBranchSink() {
290:                localSink.reset();
291:            }
292:
293:            public BufferSink insertLocalRootSink() {
294:                Debug.assertFalse(forkMerger == null,
295:                        "insertLocalRootSink() must only be called for "
296:                                + "nodes with multiple children");
297:
298:                final BufferSink localRoot = new BufferSink(null);
299:                forkMerger.setParent(localRoot);
300:
301:                return localRoot;
302:            }
303:
304:            public void removeLocalRootSink() {
305:                Debug.assertFalse(forkMerger == null,
306:                        "removeLocalRootSink() must only be called for "
307:                                + "nodes with multiple children");
308:
309:                forkMerger.setParent(branchSink);
310:            }
311:
312:            /** makes the given node a child of this node.
313:             */
314:            public void add(Node child) {
315:                child.siblingNr = children.size();
316:                children.add(child);
317:                child.parent = this ;
318:                proof.fireProofExpanded(this );
319:            }
320:
321:            /** removes child/parent relationship between this node and its
322:             * parent; if this node is root nothing happens.
323:             */
324:            public void remove() {
325:                if (parent != null) {
326:                    parent.remove(this );
327:                }
328:            }
329:
330:            /** removes child/parent relationship between the given node and
331:             * this node; if the given node is not child of this node,
332:             * nothing happens and then and only then false is returned.
333:             * @return false iff the given node was not child of this node and
334:             * nothing has been done.
335:             */
336:            public boolean remove(Node child) {
337:                if (children.remove(child)) {
338:                    child.parent = null;
339:
340:                    final ListIterator it = children
341:                            .listIterator(child.siblingNr);
342:                    while (it.hasNext()) {
343:                        ((Node) it.next()).siblingNr--;
344:                    }
345:                    child.siblingNr = -1;
346:                    proof().fireProofPruned(this , child);
347:                    return true;
348:                } else {
349:                    return false;
350:                }
351:            }
352:
353:            /**
354:             * computes the leaves of the current subtree and returns them
355:             */
356:            private List leaves() {
357:                final List leaves = new LinkedList();
358:                final LinkedList nodesToCheck = new LinkedList();
359:                nodesToCheck.add(this );
360:                while (!nodesToCheck.isEmpty()) {
361:                    final Node n = (Node) nodesToCheck.removeFirst();
362:                    if (n.leaf()) {
363:                        leaves.add(n);
364:                    } else {
365:                        nodesToCheck.addAll(0, n.children);
366:                    }
367:                }
368:                return leaves;
369:            }
370:
371:            /** 
372:             * returns an iterator for the leaves of the subtree below this
373:             * node. The computation is called at every call!
374:             */
375:            public IteratorOfNode leavesIterator() {
376:                return new NodeIterator(leaves().iterator());
377:            }
378:
379:            /** returns an iterator for the direct children of this node.
380:             */
381:            public IteratorOfNode childrenIterator() {
382:                return new NodeIterator(children.iterator());
383:            }
384:
385:            /** returns number of children */
386:            public int childrenCount() {
387:                return children.size();
388:            }
389:
390:            /** returns i-th child */
391:            public Node child(int i) {
392:                return (Node) (children.get(i));
393:            }
394:
395:            /**
396:             * @return the number of the node <code>p_node</code>, if it is a
397:             * child of this node (starting with <code>0</code>),
398:             * <code>-1</code> otherwise
399:             */
400:            public int getChildNr(Node p_node) {
401:                int res = 0;
402:                IteratorOfNode it = childrenIterator();
403:
404:                while (it.hasNext()) {
405:                    if (it.next() == p_node)
406:                        return res;
407:                    ++res;
408:                }
409:
410:                return -1;
411:            }
412:
413:            /** helps toString method 
414:             * @param prefix needed to keep track if a line has to be printed
415:             * @param tree the tree representation we want to add this subtree
416:             " @param preEnumeration the enumeration of the parent without the
417:             * last number
418:             * @param postNr the last number of the parents enumeration 
419:             * @param maxNr the number of nodes at this level
420:             * @param ownNr the place of this node at this level
421:             */
422:
423:            private StringBuffer toString(String prefix, StringBuffer tree,
424:                    String preEnumeration, int postNr, int maxNr, int ownNr) {
425:                IteratorOfNode childrenIt = childrenIterator();
426:                // Some constants
427:                String frontIndent = (maxNr > 1 ? " " : "");
428:                String backFill = "   "; // same length as connectNode without
429:                // frontIndent 
430:                String connectNode = (maxNr > 1 ? frontIndent + "+--" : "");
431:                String verticalLine = (maxNr > 1 ? frontIndent + "|" + backFill
432:                        : " |");
433:
434:                // get enumeration
435:                String newEnumeration = preEnumeration;
436:                int newPostNr = 0;
437:                if (maxNr > 1) {
438:                    newEnumeration += postNr + "." + ownNr + ".";
439:                    newPostNr = 1;
440:                } else {
441:                    newPostNr = postNr + ownNr;
442:                }
443:
444:                // node is printed
445:
446:                if (postNr != 0) { // not starting node (usually not root)
447:                    // prefix is appended twice in order to get an
448:                    // empty line between two nodes
449:                    tree.append(prefix);
450:                    tree.append(verticalLine);
451:                    tree.append("\n");
452:                    tree.append(prefix);
453:                    // indent node
454:                    tree.append(connectNode);
455:                }
456:
457:                tree.append("(" + newEnumeration + newPostNr + ") "
458:                        + sequent().toString() + "\n");
459:
460:                // create new prefix
461:                if (ownNr < maxNr) {
462:                    // connect node with next node of same level
463:                    prefix += verticalLine;
464:                } else if (ownNr == maxNr && maxNr > 1) {
465:                    // last node of level no further connection
466:                    prefix += frontIndent + " " + backFill;
467:                } else if (ownNr != maxNr && maxNr <= 1) {
468:                    prefix = "";
469:                }
470:
471:                // print subtrees
472:                int childId = 0;
473:                while (childrenIt.hasNext()) {
474:                    childId++;
475:                    childrenIt.next().toString(prefix, tree, newEnumeration,
476:                            newPostNr, children.size(), childId);
477:                }
478:
479:                return tree;
480:            }
481:
482:            public String toString() {
483:                StringBuffer tree = new StringBuffer();
484:                return "\n" + toString("", tree, "", 0, 0, 1);
485:            }
486:
487:            public String name() { // XXX this is called way too often -- cache stuff!
488:
489:                RuleApp rap = getAppliedRuleApp();
490:                if (rap == null) {
491:                    Goal goal = proof.getGoal(this );
492:                    if (goal == null
493:                            || proof().getUserConstraint().displayClosed(this ))
494:                        return "Closed goal";
495:                    else
496:                        return "OPEN GOAL";
497:                }
498:                if (rap.rule() == null)
499:                    return "rule application without rule";
500:
501:                if (nodeInfo.getFirstStatementString() != null) {
502:                    return nodeInfo.getFirstStatementString();
503:                }
504:
505:                String text = rap.rule().displayName();
506:                if (text == null) {
507:                    text = "rule without name";
508:                }
509:                return text;
510:            }
511:
512:            private static Vector reuseCandidates = new Vector(20);
513:
514:            public static Iterator reuseCandidatesIterator() {
515:                return reuseCandidates.iterator();
516:            }
517:
518:            public static int reuseCandidatesNumber() {
519:                return reuseCandidates.size();
520:            }
521:
522:            public void markReuseCandidate() {
523:                reuseCandidate++;
524:                reuseCandidates.add(this );
525:            }
526:
527:            public void markPersistentCandidate() {
528:                persistentCandidate = true;
529:            }
530:
531:            public void unmarkReuseCandidate() {
532:                if ((reuseCandidate > 1) || !persistentCandidate) {
533:                    reuseCandidate--;
534:                    reuseCandidates.remove(this );
535:                }
536:            }
537:
538:            public static void clearReuseCandidates() {
539:                Enumeration en = reuseCandidates.elements();
540:                while (en.hasMoreElements()) {
541:                    Node n = (Node) en.nextElement();
542:                    n.reuseCandidate = 0;
543:                    n.persistentCandidate = false;
544:                }
545:                reuseCandidates = new Vector(20);
546:            }
547:
548:            public static void clearReuseCandidates(Proof p) {
549:                Enumeration en = reuseCandidates.elements();
550:                while (en.hasMoreElements()) {
551:                    Node n = (Node) en.nextElement();
552:                    if (n.proof() == p)
553:                        reuseCandidates.remove(n);
554:                }
555:            }
556:
557:            public boolean isReuseCandidate() {
558:                return reuseCandidate > 0;
559:            }
560:
561:            public void setReuseSource(ReusePoint rp) {
562:                reuseSource = rp;
563:            }
564:
565:            public ReusePoint getReuseSource() {
566:                return reuseSource;
567:            }
568:
569:            /**
570:             * checks if the parent has this node as child and continues recursively
571:             * with the children of this node.
572:             * @return true iff the parent of this node has this node as child and
573:             * this condition holds also for the own children.
574:             */
575:            public boolean sanityCheckDoubleLinks() {
576:                if (!root()) {
577:                    if (!parent().children.contains(this )) {
578:                        return false;
579:                    }
580:                    if (parent.proof() != proof()) {
581:                        return false;
582:                    }
583:                }
584:                if (!leaf()) {
585:                    IteratorOfNode it = childrenIterator();
586:                    while (it.hasNext()) {
587:                        if (!it.next().sanityCheckDoubleLinks())
588:                            return false;
589:                    }
590:                }
591:                return true;
592:            }
593:
594:            public Constraint getClosureConstraint() {
595:                return localSink.getConstraint();
596:            }
597:
598:            public void addClosureConstraint(Constraint c) {
599:                localSink.put(c);
600:            }
601:
602:            public void addRestrictedMetavariable(Metavariable mv) {
603:                localSink.addRestriction(mv);
604:            }
605:
606:            public SetOfMetavariable getRestrictedMetavariables() {
607:                if (branchSink instanceof  Restricter)
608:                    return ((Restricter) branchSink).getRestrictions();
609:                else
610:                    return SetAsListOfMetavariable.EMPTY_SET;
611:            }
612:
613:            public BufferSink getRootSink() {
614:                return rootSink;
615:            }
616:
617:            public Sink getBranchSink() {
618:                return branchSink;
619:            }
620:
621:            /**
622:             * This is called by "BranchRestricter" to indicate that the
623:             * subtree below this Node is closed
624:             */
625:            public void subtreeCompletelyClosed() {
626:                proof().subtreeCompletelyClosed(this );
627:            }
628:
629:            public void setClosed() {
630:                final LinkedList subTreeNodes = new LinkedList();
631:                subTreeNodes.add(this );
632:                while (!subTreeNodes.isEmpty()) {
633:                    final Node n = (Node) subTreeNodes.removeFirst();
634:                    n.closed = true;
635:                    subTreeNodes.addAll(n.children);
636:                }
637:            }
638:
639:            public boolean isClosed() {
640:                return closed;
641:            }
642:
643:            /**
644:             * retrieves number of nodes
645:             */
646:            public int countNodes() {
647:                int nodes = 1 + children.size();
648:                final LinkedList nodesToAdd = (LinkedList) ((LinkedList) children)
649:                        .clone();
650:                while (!nodesToAdd.isEmpty()) {
651:                    final Node n = (Node) nodesToAdd.removeFirst();
652:                    nodesToAdd.addAll(n.children);
653:                    nodes += n.children.size();
654:                }
655:                return nodes;
656:            }
657:
658:            /**
659:             * retrieves number of branches
660:             */
661:            public int countBranches() {
662:                return leaves().size();
663:            }
664:
665:            public int serialNr() {
666:                return serialNr;
667:            }
668:
669:            /**
670:             * returns the sibling number of this node or <tt>-1</tt> if
671:             * it is the root node
672:             * @return the sibling number of this node or <tt>-1</tt> if
673:             * it is the root node
674:             */
675:            public int siblingNr() {
676:                return siblingNr;
677:            }
678:
679:            // inner iterator class 
680:            private class NodeIterator implements  IteratorOfNode {
681:                private Iterator it;
682:
683:                NodeIterator(Iterator it) {
684:                    this .it = it;
685:                }
686:
687:                public boolean hasNext() {
688:                    return it.hasNext();
689:                }
690:
691:                public Node next() {
692:                    return (Node) it.next();
693:                }
694:            }
695:
696:            private int getIntroducedRulesCount() {
697:                int c = 0;
698:
699:                if (parent != null) {
700:                    c = parent.getIntroducedRulesCount();
701:                }
702:
703:                return c + localIntroducedRules.size();
704:            }
705:
706:            public int getUniqueTacletNr() {
707:                return getIntroducedRulesCount();
708:            }
709:
710:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.