Source Code Cross Referenced for ReusePoint.java in  » Testing » KeY » de » uka » ilkd » key » proof » reuse » 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.reuse 
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.reuse;
012:
013:        import java.util.Hashtable;
014:        import java.util.LinkedList;
015:        import java.util.Vector;
016:
017:        import org.apache.log4j.Logger;
018:
019:        import de.uka.ilkd.key.collection.SLListOfString;
020:        import de.uka.ilkd.key.gui.KeYMediator;
021:        import de.uka.ilkd.key.java.*;
022:        import de.uka.ilkd.key.java.reference.ExecutionContext;
023:        import de.uka.ilkd.key.java.statement.MethodFrame;
024:        import de.uka.ilkd.key.logic.*;
025:        import de.uka.ilkd.key.logic.op.*;
026:        import de.uka.ilkd.key.proof.*;
027:        import de.uka.ilkd.key.rule.*;
028:        import de.uka.ilkd.key.rule.inst.*;
029:        import de.uka.ilkd.key.util.ExtList;
030:
031:        public class ReusePoint implements  Comparable {
032:
033:            Node templateNode;
034:            Goal targetGoal;
035:            int score = 0;
036:            PosInOccurrence targetPos;
037:            RuleApp templateApp;
038:            RuleApp reuseApp;
039:            /** the rule involved is not part of the standard set */
040:            private boolean goalLocalRule = false;
041:
042:            private String s = "";
043:
044:            private static Logger reuseLogger = Logger
045:                    .getLogger("key.proof.reuse");
046:
047:            private ReusePoint(ReusePoint other) {
048:                this .templateNode = other.templateNode;
049:                this .targetGoal = other.targetGoal;
050:                this .goalLocalRule = other.goalLocalRule;
051:                templateApp = templateNode.getAppliedRuleApp();
052:            }
053:
054:            public ReusePoint(Node templateNode, Goal targetGoal) {
055:                this .templateNode = templateNode;
056:                this .targetGoal = targetGoal;
057:                templateApp = templateNode.getAppliedRuleApp();
058:            }
059:
060:            public ReusePoint initialize(PosInOccurrence targetPos,
061:                    RuleApp tentativeApp, KeYMediator medi) {
062:                ReusePoint result = new ReusePoint(this );
063:                result.setTargetPos(targetPos);
064:                RuleApp targetApp = result.getTargetApp(tentativeApp, medi);
065:                if (targetApp == null)
066:                    return null;
067:                result.setReuseApp(targetApp);
068:                result.compare(result.sourceTerm(), targetPos.subTerm());
069:                if (templateApp instanceof  TacletApp) {
070:                    result.compareIf((TacletApp) templateApp,
071:                            (TacletApp) targetApp);
072:                }
073:                return result;
074:            }
075:
076:            public ReusePoint initializeNoFind(RuleApp tentativeApp,
077:                    KeYMediator medi) {
078:                ReusePoint result = new ReusePoint(this );
079:                RuleApp targetApp = result.getTargetApp(tentativeApp, medi);
080:                if (targetApp == null)
081:                    return null;
082:                result.setReuseApp(targetApp);
083:                result.compareNoFind();
084:                return result;
085:            }
086:
087:            public Goal target() {
088:                return targetGoal;
089:            }
090:
091:            public Node source() {
092:                return templateNode;
093:            }
094:
095:            public RuleApp getApp() {
096:                return templateApp;
097:            }
098:
099:            public Term sourceTerm() {
100:                return templateApp.posInOccurrence().subTerm();
101:            }
102:
103:            private void setTargetPos(PosInOccurrence pos) {
104:                this .targetPos = pos;
105:            }
106:
107:            public PosInOccurrence getTargetPos() {
108:                return targetPos;
109:            }
110:
111:            private void setReuseApp(RuleApp app) {
112:                reuseApp = app;
113:            }
114:
115:            public RuleApp getReuseApp() {
116:                return reuseApp;
117:            }
118:
119:            public void setGoalLocal(boolean b) {
120:                goalLocalRule = b;
121:            }
122:
123:            private RuleApp getTargetApp(RuleApp tentativeApp, KeYMediator medi) {
124:                if (templateApp instanceof  TacletApp) {
125:                    TacletApp result = (TacletApp) tentativeApp;
126:
127:                    //if (result.tryToInstantiate(medi.getServices())!=null)
128:                    //System.err.println(result);         
129:                    //         result = result.tryToInstantiate(medi.getServices());
130:
131:                    //if (result.rule().name().toString().equals("int_induction")) return result;
132:
133:                    // 1st pass
134:                    IteratorOfSchemaVariable it = result.uninstantiatedVars()
135:                            .iterator();
136:                    while (it.hasNext()) {
137:                        SVInstantiations insts = ((TacletApp) templateApp)
138:                                .instantiations();
139:                        SchemaVariable sv = it.next();
140:                        SchemaVariable svTemplate;
141:
142:                        if (goalLocalRule) {
143:                            svTemplate = insts.lookupVar(sv.name());
144:                        } else {
145:                            svTemplate = sv;
146:                        }
147:
148:                        String text = "";
149:                        if (sv.isVariableSV()) {
150:                            Object o = insts.getInstantiation(svTemplate);
151:                            reuseLogger.info(result.rule().name()
152:                                    + ": Copying instantiation of " + o
153:                                    + " for " + sv);
154:
155:                            if (o == null) {
156:                                text = nameSuggestion(sv, medi.getServices(),
157:                                        (TacletApp) tentativeApp);
158:                            } else {
159:                                try {
160:                                    text = ProofSaver.printTerm((Term) o,
161:                                            templateNode.proof().getServices())
162:                                            .toString();
163:                                } catch (Exception e) {
164:                                    System.err.println("Missing " + sv
165:                                            + " from "
166:                                            + tentativeApp.rule().name());
167:                                    return null;
168:                                }
169:                            }
170:                            result = ProblemLoader.parseSV1(result, sv, text,
171:                                    medi.getServices());
172:                        } else {
173:                            // leave for 2nd pass
174:                        }
175:                    }
176:
177:                    // 2nd pass
178:                    it = result.uninstantiatedVars().iterator();
179:                    SVInstantiations insts = ((TacletApp) templateApp)
180:                            .instantiations();
181:                    while (it.hasNext()) {
182:                        SchemaVariable sv = it.next();
183:                        SchemaVariable svTemplate;
184:                        if (goalLocalRule) {
185:                            svTemplate = insts.lookupVar(sv.name());
186:                        } else {
187:                            svTemplate = sv;
188:                        }
189:
190:                        InstantiationEntry o = insts.interesting().get(
191:                                svTemplate);
192:
193:                        if (result != null) {
194:                            reuseLogger.info(result.rule().name()
195:                                    + ": Copying instantiation of " + o
196:                                    + " for " + sv);
197:                        }
198:
199:                        String text = "";
200:                        if (o instanceof  TermInstantiation) {
201:                            text = ProofSaver.printTerm(
202:                                    ((TermInstantiation) o).getTerm(),
203:                                    templateNode.proof().getServices())
204:                                    .toString();
205:                        } else if (o instanceof  ProgramInstantiation) {
206:                            text = ProofSaver
207:                                    .printProgramElement(((ProgramInstantiation) o)
208:                                            .getProgramElement());
209:                        } else if (o instanceof  ListInstantiation) {
210:                            text = ProofSaver.printListInstantiation(
211:                                    ((ListInstantiation) o).getList(),
212:                                    templateNode.proof().getServices());
213:                        } else if (o == null) {
214:                            //               throw new IllegalStateException(
215:                            //                   "Null InstantiationEntry for "+sv+" in "+templateApp);
216:                            text = nameSuggestion(sv, medi.getServices(),
217:                                    (TacletApp) tentativeApp);
218:                        } else {
219:                            System.err
220:                                    .println("What the hell is this instantiation? "
221:                                            + sv + " of type " + o.getClass());
222:                            text = nameSuggestion(sv, medi.getServices(),
223:                                    (TacletApp) tentativeApp);
224:                        }
225:                        if (text == null) {
226:                            return null;
227:                        }
228:                        try {
229:                            result = ProblemLoader.parseSV2(result, sv, text,
230:                                    targetGoal);
231:                        } catch (IllegalInstantiationException e) {
232:                            result = null;
233:                        }
234:                    }
235:
236:                    return result;
237:
238:                } else if (templateApp instanceof  BuiltInRuleApp) {
239:                    IteratorOfRuleApp it = targetGoal.ruleAppIndex()
240:                            .getBuiltInRule(targetGoal, targetPos,
241:                                    medi.getUserConstraint().getConstraint())
242:                            .iterator();
243:                    RuleApp result = null;
244:                    RuleApp tmp;
245:                    while (it.hasNext()) {
246:                        tmp = it.next();
247:                        if (tmp.rule().equals(templateApp.rule())) {
248:                            if (result != null)
249:                                throw new RuntimeException(templateApp.rule()
250:                                        .name()
251:                                        + ": found more than 1 app");
252:                            else
253:                                result = tmp;
254:                        }
255:                    }
256:                    if (result == null)
257:                        System.err.println(templateApp.rule().name()
258:                                + ": found 0 apps -- too bad!");
259:                    return result;
260:                } else
261:                    throw new RuntimeException(templateApp.rule().name()
262:                            + ": neither TacletApp nor BuiltinRuleApp");
263:            }
264:
265:            private String nameSuggestion(SchemaVariable sv, Services services,
266:                    TacletApp app) {
267:                String text;
268:                if (sv.isProgramSV()) {
269:                    text = services.getVariableNamer()
270:                            .getSuggestiveNameProposalForProgramVariable(
271:                                    (ProgramSV) sv, app, targetGoal, services,
272:                                    SLListOfString.EMPTY_LIST);
273:                } else {
274:                    text = VariableNameProposer.DEFAULT.getNameProposal(sv
275:                            .name().toString().replaceAll("#", ""), services,
276:                            targetGoal.node());
277:                }
278:                return text;
279:            }
280:
281:            public int score() {
282:                return score;
283:            }
284:
285:            public boolean notGoodEnough() {
286:                return (score < -72);
287:            }
288:
289:            /** implements Comparable. Sorts in descending score order. */
290:            public int compareTo(Object o) {
291:                ReusePoint p1 = (ReusePoint) o;
292:                if (score > p1.score())
293:                    return -1;
294:                if (score < p1.score())
295:                    return 1;
296:                return 0;
297:            }
298:
299:            ExtList children(NonTerminalProgramElement p) {
300:                ExtList ch = new ExtList();
301:                for (int k = 0; k < p.getChildCount(); k++)
302:                    ch.add(p.getChildAt(k));
303:                return ch;
304:            }
305:
306:            int diffJava(JavaProgramElement x, JavaProgramElement y) {
307:                StatementCollector c1 = new StatementCollector(templateNode
308:                        .proof(), x);
309:                StatementCollector c2 = new StatementCollector(targetGoal
310:                        .proof(), y);
311:                c1.start();
312:                c2.start();
313:                DiffMyers d = new DiffMyers(c1.result(), c2.result());
314:                reuseLogger.debug(c1.result());
315:                reuseLogger.debug(c2.result());
316:                DiffMyers.change diff = d.diff_2();
317:                reuseLogger.debug(diff);
318:                if (diff != null)
319:                    return diff.diminishingPenalty();
320:                else
321:                    return 0;
322:            }
323:
324:            int scoreLogicalFindEqualsMod(Term x, Term y) {
325:                if (x.depth() == y.depth()) {
326:                    if (x.toString().equals(y.toString()))
327:                        return 10;
328:                }
329:                if (x.equalsModRenaming(y)) {
330:                    //         System.err.println("1:"+x+"<->"+y+" ["+x.depth());
331:                    return 30;
332:                } else
333:                    return -10;
334:            }
335:
336:            int diffLogical(Term x, Term y) {
337:                int this Score;
338:                Vector xsig = new Vector(20, 20);
339:                Vector ysig = new Vector(20, 20);
340:                Hashtable xDiamonds = new Hashtable(5);
341:                Hashtable yDiamonds = new Hashtable(5);
342:                createReuseSignature(x, xsig, xDiamonds);
343:                createReuseSignature(y, ysig, yDiamonds);
344:                reuseLogger.debug(xsig);
345:                reuseLogger.debug(ysig);
346:                DiffMyers d = new DiffMyers(xsig, ysig);
347:                DiffMyers.change diff = d.diff_2();
348:                reuseLogger.debug(diff);
349:                if (diff != null)
350:                    this Score = diff.uniformPenalty();
351:                else
352:                    this Score = 0;
353:
354:                DiffMyers.mapping map = d.getMapping();
355:                while (map != null) {
356:                    int from = map.from();
357:                    int to = map.to();
358:                    if (xsig.elementAt(from).equals("diamond")) {
359:                        reuseLogger.debug("diamond " + from + "<->" + to);
360:                        Term d1 = (Term) xDiamonds.get(new Integer(from));
361:                        Term d2 = (Term) yDiamonds.get(new Integer(to));
362:                        int diamondScore = diffJava(d1.executableJavaBlock()
363:                                .program(), d2.executableJavaBlock().program()) / 4;
364:                        //            System.err.println(d1);
365:                        //            System.err.println(d2);
366:                        reuseLogger.debug("Diamond correspondence penalty "
367:                                + diamondScore);
368:                        this Score += diamondScore;
369:
370:                    }
371:
372:                    map = map.next();
373:                }
374:                this Score -= Math.abs(xDiamonds.size() - yDiamonds.size()) * 30;
375:
376:                return this Score;
377:            }
378:
379:            int diffPosInTerm(PosInTerm x, PosInTerm y) {
380:                int this Score;
381:
382:                DiffMyers d = new DiffMyers(x, y);
383:                DiffMyers.change diff = d.diff_2();
384:                reuseLogger.debug(diff);
385:                if (diff != null)
386:                    this Score = diff.uniformPenalty();
387:                else
388:                    this Score = 0;
389:                return this Score;
390:            }
391:
392:            void compareNoFind() {
393:                reuseLogger.info("*-");
394:                //System.err.println("Comparing terms "+x+"<->"+y);
395:                int localScore;
396:                localScore = scoreConnectNoFind(templateNode, targetGoal.node());
397:                //      localScore += scoreConnectSemiseq();
398:                reuseLogger.info("Connectivity reward " + localScore);
399:                score += localScore;
400:                s = s + "Connectivity: " + localScore + "\n";
401:
402:                localScore = scoreSiblingNr(templateNode, targetGoal.node());
403:                reuseLogger.info("Sibling order penalty " + localScore);
404:                score += localScore;
405:                s = s + "Sibling order penalty: " + localScore + "\n";
406:
407:                reuseLogger.info("Total score " + score);
408:                s = s + "-------\n";
409:                s = s + "Total score: " + score + "\n";
410:                s = s + "Reuse source: " + templateNode.serialNr() + "\n";
411:            }
412:
413:            void compare(Term x, Term y) {
414:                reuseLogger.info("* " + getApp().rule().name());
415:                //System.err.println("Comparing terms "+x+"<->"+y);
416:                int localScore;
417:                JavaBlock jx = x.executableJavaBlock();
418:                JavaBlock jy = y.executableJavaBlock();
419:                if (jx == JavaBlock.EMPTY_JAVABLOCK
420:                        || jy == JavaBlock.EMPTY_JAVABLOCK) {
421:
422:                    // not a symbolic execution rule
423:                    localScore = scoreLogicalFindEqualsMod(x, y);
424:                    reuseLogger.info("By equalsModRenaming on find "
425:                            + localScore);
426:                    score += localScore;
427:                    s = s + "By equalsModRenaming on find " + localScore + "\n";
428:
429:                    localScore = diffLogical(templateApp.posInOccurrence()
430:                            .constrainedFormula().formula(), targetPos
431:                            .constrainedFormula().formula());
432:                    reuseLogger.info("By diff on complete formulae "
433:                            + localScore);
434:                    score += localScore;
435:                    s = s + "By diff on complete formulae " + localScore + "\n";
436:
437:                    localScore = diffPosInTerm(templateApp.posInOccurrence()
438:                            .posInTerm(), targetPos.posInTerm());
439:                    reuseLogger.info("By diff on PosInTerm " + localScore);
440:                    score += localScore;
441:                    s = s + "By diff on PosInTerm " + localScore + "\n";
442:
443:                } else { // program similarity
444:                    if (jy.size() > 1) {
445:                        localScore = diffJava(jx.program(), jy.program());
446:                        reuseLogger.info("Scored java diff " + localScore);
447:                        score += localScore;
448:                        s = s + "Program similarity " + localScore + "\n";
449:                    } else { // small program -- look at whole formula
450:                        localScore = diffLogical(x, y);
451:                        reuseLogger
452:                                .info("Scored whole formula (small program) "
453:                                        + localScore);
454:                        score += localScore;
455:                        s = s + "By whole formula (small program) "
456:                                + localScore + "\n";
457:                    }
458:                }
459:
460:                localScore = scoreConnect(templateNode, targetGoal.node());
461:                //      localScore += scoreConnectSemiseq();
462:                reuseLogger.info("Connectivity reward " + localScore);
463:                score += localScore;
464:                s = s + "Connectivity: " + localScore + "\n";
465:
466:                localScore = scoreSiblingNr(templateNode, targetGoal.node());
467:                reuseLogger.info("Sibling order penalty " + localScore);
468:                score += localScore;
469:                s = s + "Sibling order penalty: " + localScore + "\n";
470:
471:                reuseLogger.info("Total score " + score);
472:                s = s + "-------\n";
473:                s = s + "Total score: " + score + "\n";
474:                s = s + "Reuse source: " + templateNode.serialNr() + "\n";
475:            }
476:
477:            void compareIf(TacletApp sourceApp, TacletApp targetApp) {
478:                ListOfIfFormulaInstantiation ifl1 = sourceApp
479:                        .ifFormulaInstantiations();
480:                ListOfIfFormulaInstantiation ifl2 = targetApp
481:                        .ifFormulaInstantiations();
482:                Term if1;
483:                ConstrainedFormula iff2;
484:                Term if2;
485:                boolean if2inAntec;
486:                try {
487:                    if1 = ifl1.head().getConstrainedFormula().formula();
488:                    if2inAntec = ((IfFormulaInstSeq) ifl2.head()).inAntec();
489:                    iff2 = ifl2.head().getConstrainedFormula();
490:                    if2 = iff2.formula();
491:                } catch (Exception e) {
492:                    return;
493:                }
494:                int i = diffLogical(if1, if2);
495:                i += scoreLogicalFindEqualsMod(if1, if2);
496:                score += (i * 0.2);
497:
498:                boolean sameFormula;
499:                PosInOccurrence findPos = targetApp.posInOccurrence();
500:
501:                sameFormula = (findPos.isInAntec() == if2inAntec)
502:                        && (findPos.constrainedFormula().equals(iff2));
503:                if (sameFormula)
504:                    score -= 40;
505:
506:                s = s + "By IF: " + score + "\n";
507:
508:            }
509:
510:            boolean connect = false;
511:
512:            public boolean isConnect() {
513:                return connect;
514:            }
515:
516:            int scoreConnect(Node templateNode, Node targetNode) {
517:                Node predecSource;
518:                Node predecTarget;
519:                try {
520:                    predecSource = templateNode.parent();
521:                    predecTarget = targetNode.parent();
522:                    if (predecTarget.getReuseSource().source() == predecSource) {
523:                        connect = true;
524:                        return 0;
525:                    } else
526:                        return -70;//-15;
527:                } catch (NullPointerException npe) {
528:                    return -1; // some ingredient is missing --> neutral score
529:                }
530:            }
531:
532:            int scoreConnectNoFind(Node templateNode, Node targetNode) {
533:                Node predecSource;
534:                Node predecTarget;
535:                try {
536:                    predecSource = templateNode.parent();
537:                    predecTarget = targetNode.parent();
538:                    if (predecTarget.getReuseSource().source() == predecSource) {
539:                        connect = true;
540:                        return 0;
541:                    } else
542:                        return -100; // kill
543:                } catch (NullPointerException npe) {
544:                    return -1; // some ingredient is missing --> too bad
545:                }
546:            }
547:
548:            int scoreSiblingNr(Node templateNode, Node targetNode) {
549:                if (templateNode.siblingNr() == targetNode.siblingNr())
550:                    return 0;
551:                else
552:                    return -1;
553:            }
554:
555:            // not used currently
556:            int scoreConnectSemiseq() {
557:                boolean b1 = templateApp.posInOccurrence().isInAntec();
558:                boolean b2 = targetPos.isInAntec();
559:                if (b1 != b2)
560:                    return -10;
561:                else
562:                    return 0;
563:            }
564:
565:            // not used currently
566:            int twoOpAboveFind() {
567:                int this Score = 0;
568:                reuseLogger.debug(targetPos.posInTerm());
569:                reuseLogger.debug(templateApp.posInOccurrence().posInTerm());
570:
571:                // the interface is worth improving...
572:                if (targetPos.up().subTerm().op() != templateApp
573:                        .posInOccurrence().up().subTerm().op())
574:                    this Score = -35;
575:                if (targetPos.up().up().subTerm().op() != templateApp
576:                        .posInOccurrence().up().up().subTerm().op())
577:                    this Score = -35;
578:
579:                reuseLogger.info("By two operators above " + this Score);
580:                return this Score;
581:            }
582:
583:            public static void createReuseSignature(Term t, Vector signature,
584:                    Hashtable diamondCollector) {
585:                if (t.op() instanceof  IUpdateOperator) {
586:                    createReuseSignature(((IUpdateOperator) t.op()).target(t),
587:                            signature, diamondCollector);
588:                    return;
589:                }
590:                String termsig = t.op().toString();
591:                //       s = s.substring(s.lastIndexOf(".")+1, s.length());
592:
593:                if ((t.op() instanceof  TermSymbol)
594:                        || (t.op() instanceof  AccessOp)) {
595:                    signature.add(t.sort().toString());
596:                    return;
597:                }
598:
599:                signature.add(termsig);
600:                if ("diamond".equals(termsig))
601:                    diamondCollector.put(new Integer(signature.size() - 1), t);
602:                //       if (s.equals("Z:int")) return;
603:                int i;
604:                for (i = 0; i < t.arity(); i++)
605:                    createReuseSignature(t.sub(i), signature, diamondCollector);
606:            }
607:
608:            public String scoringInfo() {
609:                return s;
610:            }
611:
612:            public String toString() {
613:                return "RP(" + score + ") " + templateApp.rule().name() + ":"
614:                        + templateNode.serialNr() + "->"
615:                        + targetGoal.node().serialNr();//" "+sourceTerm();
616:            }
617:
618:            //***************************************************************
619:
620:            class StatementCollector extends
621:                    de.uka.ilkd.key.java.visitor.JavaASTWalker {
622:
623:                Proof proof;
624:
625:                StatementCollector(Proof proof, ProgramElement root) {
626:                    super (root);
627:                    this .proof = proof;
628:                }
629:
630:                Vector result = new Vector(20, 20);
631:                LinkedList executionContext = new LinkedList();
632:
633:                protected void walk(ProgramElement node) {
634:                    if (node instanceof  MethodFrame) {
635:                        executionContext.addFirst(((MethodFrame) node)
636:                                .getExecutionContext());
637:                    }
638:                    if (node != root())
639:                        doAction(node);
640:                    if (node instanceof  NonTerminalProgramElement) {
641:                        NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
642:                        for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
643:                            walk(nonTerminalNode.getChildAt(i));
644:                        }
645:                    }
646:                    if (node != root())
647:                        doLeaveAction(node);
648:                    if (node instanceof  MethodFrame) {
649:                        executionContext.removeFirst();
650:                    }
651:                }
652:
653:                protected void doAction(ProgramElement node) {
654:                    if (node instanceof  StatementBlock) {
655:                        //            result.add("{");
656:                        return;
657:                    }
658:                    //         if (node instanceof Statement) result.add(node);
659:                    if (node instanceof  Statement) {
660:                        final ExecutionContext ec = (ExecutionContext) (executionContext
661:                                .size() > 0 ? executionContext.getFirst()
662:                                : null);
663:                        result.add(((JavaProgramElement) node).reuseSignature(
664:                                proof.getServices(), ec));
665:                    }
666:                }
667:
668:                protected void doLeaveAction(ProgramElement node) {
669:                    //         if (node instanceof StatementBlock) result.add("}");
670:                }
671:
672:                Vector result() {
673:                    return result;
674:                }
675:            }
676:
677:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.