Source Code Cross Referenced for VariableNamer.java in  » Testing » KeY » de » uka » ilkd » key » logic » 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.logic 
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:        // This file is part of KeY - Integrated Deductive Software Design
009:        // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010:        //                         Universitaet Koblenz-Landau, Germany
011:        //                         Chalmers University of Technology, Sweden
012:        //
013:        // The KeY system is protected by the GNU General Public License.
014:        // See LICENSE.TXT for details.
015:        //
016:        //
017:
018:        package de.uka.ilkd.key.logic;
019:
020:        import java.util.HashMap;
021:
022:        import de.uka.ilkd.key.collection.IteratorOfString;
023:        import de.uka.ilkd.key.collection.ListOfString;
024:        import de.uka.ilkd.key.java.*;
025:        import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026:        import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
027:        import de.uka.ilkd.key.java.declaration.VariableSpecification;
028:        import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
029:        import de.uka.ilkd.key.java.reference.ExecutionContext;
030:        import de.uka.ilkd.key.java.statement.EmptyStatement;
031:        import de.uka.ilkd.key.java.statement.MethodFrame;
032:        import de.uka.ilkd.key.java.visitor.JavaASTWalker;
033:        import de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor;
034:        import de.uka.ilkd.key.logic.op.*;
035:        import de.uka.ilkd.key.logic.sort.ArraySort;
036:        import de.uka.ilkd.key.logic.sort.PrimitiveSort;
037:        import de.uka.ilkd.key.logic.sort.ProgramSVSort;
038:        import de.uka.ilkd.key.logic.sort.Sort;
039:        import de.uka.ilkd.key.proof.Goal;
040:        import de.uka.ilkd.key.proof.InstantiationProposer;
041:        import de.uka.ilkd.key.proof.Node;
042:        import de.uka.ilkd.key.proof.ProofSaver;
043:        import de.uka.ilkd.key.rule.IteratorOfTacletGoalTemplate;
044:        import de.uka.ilkd.key.rule.NewVarcond;
045:        import de.uka.ilkd.key.rule.RewriteTacletGoalTemplate;
046:        import de.uka.ilkd.key.rule.TacletApp;
047:        import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
048:        import de.uka.ilkd.key.rule.inst.SVInstantiations;
049:
050:        /**
051:         * Responsible for program variable naming issues.
052:         */
053:        public abstract class VariableNamer implements  InstantiationProposer {
054:
055:            //-------------------------------------------------------------------------
056:            //member variables
057:            //-------------------------------------------------------------------------
058:
059:            /**
060:             * default basename for variable name proposals
061:             */
062:            private static final String DEFAULT_BASENAME = "var";
063:
064:            /**
065:             * name of the counter object used for temporary name proposals
066:             */
067:            private static final String TEMPCOUNTER_NAME = "VarNamerCnt";
068:
069:            /**
070:             * status of suggestive name proposing
071:             */
072:            private static boolean suggestive_off = true;
073:
074:            /**
075:             * pointer to services object
076:             */
077:            private final Services services;
078:
079:            protected HashMap map = new HashMap();
080:            protected HashMap renamingHistory = new HashMap();
081:
082:            //-------------------------------------------------------------------------
083:            //constructors
084:            //-------------------------------------------------------------------------
085:
086:            /**
087:             * @param services pointer to services object
088:             */
089:            public VariableNamer(Services services) {
090:                this .services = services;
091:            }
092:
093:            //-------------------------------------------------------------------------
094:            //internal: general stuff
095:            //-------------------------------------------------------------------------
096:
097:            /**
098:             * determines the passed ProgramElementName's basename and index (ignoring
099:             * temporary indices)
100:             */
101:            protected BasenameAndIndex getBasenameAndIndex(
102:                    ProgramElementName name) {
103:                BasenameAndIndex result = new BasenameAndIndex();
104:
105:                if (name instanceof  PermIndProgramElementName) {
106:                    result.basename = ((IndProgramElementName) name)
107:                            .getBaseName();
108:                    result.index = ((IndProgramElementName) name).getIndex();
109:                } else if (name instanceof  TempIndProgramElementName) {
110:                    result.basename = ((IndProgramElementName) name)
111:                            .getBaseName();
112:                    result.index = 0;
113:                } else {
114:                    result.basename = name.toString();
115:                    result.index = 0;
116:                }
117:
118:                //for debugging
119:                /*if(!(name instanceof IndProgramElementName)
120:                     && parseName(name.toString()) instanceof IndProgramElementName) {
121:                    System.out.println("VN Debug error: inspected name \"" + name
122:                    			+ "\" has " + name.getClass());
123:                }*/
124:
125:                return result;
126:            }
127:
128:            public HashMap getRenamingMap() {
129:                return renamingHistory;
130:            }
131:
132:            /**
133:             * returns the subterm containing a java block, or null
134:             * (helper for getProgramFromPIO())
135:             */
136:            private Term findProgramInTerm(Term term) {
137:                if (term.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
138:                    return term;
139:                }
140:                for (int i = 0; i < term.arity(); i++) {
141:                    Term subterm = findProgramInTerm(term.sub(i));
142:                    if (subterm != null) {
143:                        return subterm;
144:                    }
145:                }
146:                return null;
147:            }
148:
149:            /**
150:             * returns the program contained in a PosInOccurrence
151:             */
152:            protected ProgramElement getProgramFromPIO(PosInOccurrence pio) {
153:                Term progTerm;
154:                if (pio != null
155:                        && (progTerm = findProgramInTerm(pio.subTerm())) != null) {
156:                    return progTerm.javaBlock().program();
157:                } else {
158:                    return new EmptyStatement();
159:                }
160:            }
161:
162:            /**
163:             * returns a NameCreationInfo representing the method stack of a
164:             * PosInOccurrence
165:             */
166:            protected NameCreationInfo getMethodStack(PosInOccurrence posOfFind) {
167:                ListOfProgramMethod list = SLListOfProgramMethod.EMPTY_LIST;
168:
169:                SourceElement element = getProgramFromPIO(posOfFind);
170:                while (element != element.getFirstElement()) {
171:                    element = element.getFirstElement();
172:
173:                    if (element instanceof  MethodFrame) {
174:                        MethodFrame frame = (MethodFrame) element;
175:                        ProgramMethod method = frame.getProgramMethod();
176:                        if (method != null) {
177:                            list = list.append(method);
178:                        }
179:                    }
180:                }
181:
182:                return new MethodStackInfo(list);
183:            }
184:
185:            /**
186:             * creates a ProgramElementName object to be used for permanent names
187:             */
188:            protected ProgramElementName createName(String basename, int index,
189:                    NameCreationInfo creationInfo) {
190:                return new PermIndProgramElementName(basename, index,
191:                        creationInfo);
192:            }
193:
194:            //-------------------------------------------------------------------------
195:            //internal: counter finding
196:            //-------------------------------------------------------------------------
197:
198:            /**
199:             * returns the maximum counter value already associated with the passed
200:             * basename in the passed list of global variables, or -1
201:             */
202:            protected int getMaxCounterInGlobals(String basename,
203:                    Globals globals) {
204:                int result = -1;
205:
206:                IteratorOfProgramElementName it = globals.iterator();
207:                while (it.hasNext()) {
208:                    ProgramElementName name = it.next();
209:                    BasenameAndIndex bai = getBasenameAndIndex(name);
210:                    if (bai.basename.equals(basename) && bai.index > result) {
211:                        result = bai.index;
212:                    }
213:                }
214:
215:                return result;
216:            }
217:
218:            /**
219:             * returns the maximum counter value already associated with the passed
220:             * basename in the passed program (ignoring temporary counters), or -1
221:             */
222:            protected int getMaxCounterInProgram(String basename,
223:                    ProgramElement program, PosInProgram posOfDeclaration) {
224:                class MyWalker extends CustomJavaASTWalker {
225:                    public String basename;
226:                    public int maxCounter = -1;
227:
228:                    public MyWalker(ProgramElement program,
229:                            PosInProgram posOfDeclaration) {
230:                        super (program, posOfDeclaration);
231:                    }
232:
233:                    protected void doAction(ProgramElement node) {
234:                        if (node instanceof  ProgramVariable) {
235:                            ProgramVariable var = (ProgramVariable) node;
236:                            ProgramElementName name = var
237:                                    .getProgramElementName();
238:                            if (!(name instanceof  TempIndProgramElementName)) {
239:                                BasenameAndIndex bai = getBasenameAndIndex(name);
240:                                if (bai.basename.equals(basename)
241:                                        && bai.index > maxCounter) {
242:                                    maxCounter = bai.index;
243:                                }
244:                            }
245:                        }
246:                    }
247:                }
248:
249:                MyWalker walker = new MyWalker(program, posOfDeclaration);
250:                walker.basename = basename;
251:                walker.start();
252:
253:                return walker.maxCounter;
254:            }
255:
256:            //-------------------------------------------------------------------------
257:            //internal: uniqueness checking
258:            //-------------------------------------------------------------------------
259:
260:            /**
261:             * tells whether a name is unique in the passed list of global variables
262:             */
263:            protected boolean isUniqueInGlobals(String name, Globals globals) {
264:                IteratorOfProgramElementName it = globals.iterator();
265:                while (it.hasNext()) {
266:                    ProgramElementName n = it.next();
267:                    if (n.toString().equals(name)) {
268:                        return false;
269:                    }
270:                }
271:                return true;
272:            }
273:
274:            /**
275:             * tells whether a name is unique in the passed program
276:             */
277:            protected boolean isUniqueInProgram(String name,
278:                    ProgramElement program, PosInProgram posOfDeclaration) {
279:                class MyWalker extends CustomJavaASTWalker {
280:                    public String nameToFind;
281:                    public boolean foundIt = false;
282:
283:                    public MyWalker(ProgramElement program,
284:                            PosInProgram posOfDeclaration) {
285:                        super (program, posOfDeclaration);
286:                    }
287:
288:                    protected void doAction(ProgramElement node) {
289:                        if (node instanceof  ProgramVariable) {
290:                            ProgramVariable var = (ProgramVariable) node;
291:                            ProgramElementName varname = var
292:                                    .getProgramElementName();
293:                            if (varname.getProgramName().equals(nameToFind)) {
294:                                foundIt = true;
295:                            }
296:                        }
297:                    }
298:                }
299:
300:                MyWalker walker = new MyWalker(program, posOfDeclaration);
301:                walker.nameToFind = name;
302:                walker.start();
303:
304:                return !walker.foundIt;
305:            }
306:
307:            //-------------------------------------------------------------------------
308:            //internal: uniform treatment of global variables
309:            //-------------------------------------------------------------------------
310:
311:            /**
312:             * creates a Globals object for use with other internal methods
313:             */
314:            protected Globals wrapGlobals(ListOfNamed globals) {
315:                return new GlobalsAsListOfNamed(globals);
316:            }
317:
318:            /**
319:             * creates a Globals object for use with other internal methods
320:             */
321:            protected Globals wrapGlobals(SetOfProgramVariable globals) {
322:                return new GlobalsAsSetOfProgramVariable(globals);
323:            }
324:
325:            //-------------------------------------------------------------------------
326:            //interface: renaming
327:            //-------------------------------------------------------------------------
328:
329:            /**
330:             * intended to be called when symbolically executing a variable declaration;
331:             * resolves any naming conflicts between the new variable and other global
332:             * variables by renaming the new variable and / or other variables
333:             * @param var the new program variable
334:             * @param goal the goal
335:             * @param posOfFind the PosInOccurrence of the currently executed program
336:             * @return the renamed version of the var parameter
337:             */
338:            public abstract ProgramVariable rename(ProgramVariable var,
339:                    Goal goal, PosInOccurrence posOfFind);
340:
341:            //-------------------------------------------------------------------------
342:            //internal: name proposals
343:            //-------------------------------------------------------------------------
344:
345:            /**
346:             * proposes a base name for a given sort
347:             */
348:            private String getBaseNameProposal(Sort sort) {
349:                String result;
350:                String name = sort.name().toString();
351:                if (sort instanceof  PrimitiveSort) {
352:                    result = name.substring(0, 1);
353:                } else if (sort instanceof  ArraySort) {
354:                    result = DEFAULT_BASENAME;
355:                } else {
356:                    int lastDotIndex = name.lastIndexOf('.');
357:                    if (lastDotIndex != -1) {
358:                        name = name.substring(lastDotIndex + 1);
359:                    }
360:                    result = name.substring(0, 1).toLowerCase()
361:                            + name.substring(1);
362:                }
363:
364:                return result;
365:            }
366:
367:            /**
368:             * proposes a unique name for the instantiation of a schema variable
369:             * (like getProposal(), but somewhat less nicely)
370:             * @param basename desired base name, or null to use default
371:             * @param sv the schema variable
372:             * @param posOfFind the PosInOccurrence containing the name's target program
373:             * @param posOfDeclaration the PosInProgram where the name will be declared
374:             *                         (or null to just be pessimistic about the scope)
375:             * @param previousProposals list of names which should be considered taken,
376:             *                          or null
377:             * @return the name proposal, or null if no proposal is available
378:             */
379:            protected ProgramElementName getNameProposalForSchemaVariable(
380:                    String basename, SortedSchemaVariable sv,
381:                    PosInOccurrence posOfFind, PosInProgram posOfDeclaration,
382:                    ListOfString previousProposals) {
383:                ProgramElementName result = null;
384:
385:                Sort svSort = sv.sort();
386:                if (svSort == ProgramSVSort.VARIABLE) {
387:                    if (basename == null || "".equals(basename)) {
388:                        basename = DEFAULT_BASENAME;
389:                    }
390:                    int cnt = getMaxCounterInProgram(basename,
391:                            getProgramFromPIO(posOfFind), posOfDeclaration) + 1;
392:
393:                    result = createName(basename, cnt, null);
394:
395:                    //avoid using a previous proposal again
396:                    if (previousProposals != null) {
397:                        boolean collision;
398:                        do {
399:                            collision = false;
400:                            IteratorOfString it = previousProposals.iterator();
401:                            while (it.hasNext()) {
402:                                String s = it.next();
403:                                if (s.equals(result.toString())) {
404:                                    result = createName(basename, ++cnt, null);
405:                                    collision = true;
406:                                    break;
407:                                }
408:                            }
409:                        } while (collision);
410:                    }
411:                }
412:
413:                return result;
414:            }
415:
416:            //-------------------------------------------------------------------------
417:            //interface: name proposals
418:            //-------------------------------------------------------------------------
419:
420:            /**
421:             * proposes a unique name; intended for use in places where the information
422:             * required by getProposal() is not available
423:             * @param basename desired base name, or null to use default
424:             * @return the name proposal
425:             */
426:            public ProgramElementName getTemporaryNameProposal(String basename) {
427:                if (basename == null || "".equals(basename)) {
428:                    basename = DEFAULT_BASENAME;
429:                }
430:                int cnt = services.getCounter(TEMPCOUNTER_NAME)
431:                        .getCountPlusPlus(null);
432:                //using null as undo anchor should be okay, since the name which the
433:                //the counter is used for is only temporary and will be changed
434:                //before the variable enters the logic
435:
436:                return new TempIndProgramElementName(basename, cnt, null);
437:            }
438:
439:            /**
440:             * proposes a unique name for the instantiation of a schema variable 
441:             * @param app the taclet app
442:             * @param var the schema variable to be instantiated
443:             * @param services not used
444:             * @param undoAnchor not used
445:             * @param previousProposals list of names which should be considered taken,
446:             *                          or null
447:             * @return the name proposal, or null if no proposal is available
448:             */
449:            public String getProposal(TacletApp app, SchemaVariable var,
450:                    Services services, Node undoAnchor,
451:                    ListOfString previousProposals) {
452:                //determine posOfDeclaration from TacletApp
453:                ContextInstantiationEntry cie = app.instantiations()
454:                        .getContextInstantiation();
455:                PosInProgram posOfDeclaration = (cie == null ? null : cie
456:                        .prefix());
457:
458:                //determine a suitable base name	
459:                String basename = null;
460:                NewVarcond nv = app.taclet().varDeclaredNew(var);
461:                if (nv != null) {
462:                    Sort sort = nv.getSort();
463:                    if (sort != null) {
464:                        basename = getBaseNameProposal(sort);
465:                    } else {
466:                        SchemaVariable psv = nv.getPeerSchemaVariable();
467:                        Object inst = app.instantiations()
468:                                .getInstantiation(psv);
469:                        if (inst instanceof  Expression) {
470:                            final ExecutionContext ec = app.instantiations()
471:                                    .getExecutionContext();
472:                            if (ec != null) {
473:                                KeYJavaType kjt = ((Expression) inst)
474:                                        .getKeYJavaType(this .services, ec);
475:                                basename = getBaseNameProposal(kjt.getSort());
476:                            } else {
477:                                // usually this should never be entered, but because of 
478:                                // naming issues we do not want nullpointer exceptions
479:                                // 'u' for unknown
480:                                basename = "u";
481:                            }
482:                        }
483:                    }
484:                }
485:
486:                //get the proposal
487:                ProgramElementName name = getNameProposalForSchemaVariable(
488:                        basename, (SortedSchemaVariable) var, app
489:                                .posInOccurrence(), posOfDeclaration,
490:                        previousProposals);
491:                return (name == null ? null : name.toString());
492:            }
493:
494:            //-------------------------------------------------------------------------
495:            //interface: uniqueness checking
496:            //-------------------------------------------------------------------------
497:
498:            /**
499:             * tells whether a name for instantiating a schema variable is unique
500:             * within its scope
501:             * @param name the name to be checked
502:             * @param sv the schema variable
503:             * @param posOfFind the PosInOccurrence of the name's target program
504:             * @param posOfDeclaration the PosInProgram where the name will be declared
505:             * @return true if the name is unique or if its uniqueness cannot be
506:             *         checked, else false
507:             */
508:            public boolean isUniqueNameForSchemaVariable(String name,
509:                    SortedSchemaVariable sv, PosInOccurrence posOfFind,
510:                    PosInProgram posOfDeclaration) {
511:                boolean result = true;
512:
513:                Sort svSort = sv.sort();
514:                if (svSort == ProgramSVSort.VARIABLE) {
515:                    result = isUniqueInProgram(name,
516:                            getProgramFromPIO(posOfFind), posOfDeclaration);
517:                }
518:
519:                return result;
520:            }
521:
522:            //-------------------------------------------------------------------------
523:            //interface: name parsing
524:            //-------------------------------------------------------------------------
525:
526:            /**
527:             * parses the passed string and creates a suitable program element name
528:             * (this does *not* make the name unique - if that is necessary, use either
529:             * getTemporaryNameProposal() or getProposal())
530:             * @param name the name as a string
531:             * @param creationInfo optional name creation info the name should carry
532:             * @param comments any comments the name should carry
533:             * @return the name as a ProgramElementName
534:             */
535:            public static ProgramElementName parseName(String name,
536:                    NameCreationInfo creationInfo, Comment[] comments) {
537:                ProgramElementName result;
538:
539:                int sepPos = name
540:                        .lastIndexOf(TempIndProgramElementName.SEPARATOR);
541:                if (sepPos > 0) {
542:                    String basename = name.substring(0, sepPos);
543:                    int index = Integer.parseInt(name.substring(sepPos + 1));
544:                    result = new TempIndProgramElementName(basename, index,
545:                            creationInfo, comments);
546:                } else {
547:                    sepPos = name
548:                            .lastIndexOf(PermIndProgramElementName.SEPARATOR);
549:                    if (sepPos > 0) {
550:                        try {
551:                            String basename = name.substring(0, sepPos);
552:                            int index = Integer.parseInt(name
553:                                    .substring(sepPos + 1));
554:                            result = new PermIndProgramElementName(basename,
555:                                    index, creationInfo, comments);
556:                        } catch (NumberFormatException e) {
557:                            result = new ProgramElementName(name, creationInfo,
558:                                    comments);
559:                        }
560:                    } else {
561:                        result = new ProgramElementName(name, creationInfo,
562:                                comments);
563:                    }
564:                }
565:
566:                return result;
567:            }
568:
569:            public static ProgramElementName parseName(String name,
570:                    NameCreationInfo creationInfo) {
571:                return parseName(name, creationInfo, new Comment[0]);
572:            }
573:
574:            public static ProgramElementName parseName(String name,
575:                    Comment[] comments) {
576:                return parseName(name, null, comments);
577:            }
578:
579:            public static ProgramElementName parseName(String name) {
580:                return parseName(name, null, new Comment[0]);
581:            }
582:
583:            //-------------------------------------------------------------------------
584:            //interface: suggestive name proposals
585:            //(taken from VarNameDeliverer.java, pretty much unchanged)
586:            //-------------------------------------------------------------------------
587:
588:            public static void setSuggestiveEnabled(boolean enabled) {
589:                suggestive_off = !enabled;
590:            }
591:
592:            // precondition: sv.sort()==ProgramSVSort.VARIABLE
593:            public String getSuggestiveNameProposalForProgramVariable(
594:                    SortedSchemaVariable sv, TacletApp app, Goal goal,
595:                    Services services, ListOfString previousProposals) {
596:                if (suggestive_off) {
597:                    return getProposal(app, sv, services, null,
598:                            previousProposals);
599:                }
600:
601:                String proposal;
602:                boolean found = false;
603:                try {
604:                    IteratorOfTacletGoalTemplate templs = app.taclet()
605:                            .goalTemplates().iterator();
606:                    RewriteTacletGoalTemplate rwgt = null;
607:                    String name = "";
608:                    while (templs.hasNext() && !found) {
609:                        rwgt = (RewriteTacletGoalTemplate) templs.next();
610:                        Term t = findProgramInTerm(rwgt.replaceWith());
611:                        ContextStatementBlock c = (ContextStatementBlock) t
612:                                .executableJavaBlock().program();
613:                        if (c.getStatementAt(0) instanceof  LocalVariableDeclaration) {
614:                            VariableSpecification v = ((LocalVariableDeclaration) c
615:                                    .getStatementAt(0)).getVariables()
616:                                    .getVariableSpecification(0);
617:
618:                            if (v.hasInitializer()) {
619:                                ProgramElement rhs = instantiateExpression(v
620:                                        .getInitializer(),
621:                                        app.instantiations(), services);
622:                                name = ProofSaver.printProgramElement(rhs);
623:                                break;
624:                            } else if (c.getStatementAt(1) instanceof  CopyAssignment) {
625:                                CopyAssignment p2 = (CopyAssignment) c
626:                                        .getStatementAt(1);
627:                                Expression lhs = p2.getExpressionAt(0);
628:                                if (lhs.equals(sv)) {
629:                                    SortedSchemaVariable rhs = (SortedSchemaVariable) p2
630:                                            .getExpressionAt(1);
631:                                    name = app.instantiations()
632:                                            .getInstantiation(rhs).toString();
633:                                    break;
634:                                }
635:                            }
636:                        }
637:
638:                    }
639:                    if ("".equals(name))
640:                        throw new Exception();
641:                    proposal = "[" + name + "]";
642:                } catch (Exception e) { // bad style, but this is really non-critical
643:                    //System.err.println(e);
644:                    //e.printStackTrace();
645:                    return getProposal(app, sv, services, null,
646:                            previousProposals);
647:                }
648:                return proposal;
649:            }
650:
651:            public String getSuggestiveNameProposalForSchemaVariable(
652:                    Expression e) {
653:                if (suggestive_off) {
654:                    return getTemporaryNameProposal(DEFAULT_BASENAME)
655:                            .toString();
656:                }
657:                return "[" + ProofSaver.printProgramElement(e) + "]";
658:            }
659:
660:            private ProgramElement instantiateExpression(ProgramElement e,
661:                    SVInstantiations svInst, Services services) {
662:                ProgramReplaceVisitor trans = new ProgramReplaceVisitor(e,
663:                        services, svInst, false);
664:                trans.start();
665:                return trans.result();
666:            }
667:
668:            //-------------------------------------------------------------------------
669:            //inner classes
670:            //-------------------------------------------------------------------------
671:
672:            /**
673:             * ProgramElementName carrying an additional index
674:             */
675:            private abstract static class IndProgramElementName extends
676:                    ProgramElementName {
677:                private final String basename;
678:                private final int index;
679:
680:                IndProgramElementName(String name, String basename, int index,
681:                        NameCreationInfo creationInfo) {
682:                    super (name, creationInfo);
683:                    this .basename = basename.intern();
684:                    this .index = index;
685:                }
686:
687:                IndProgramElementName(String name, String basename, int index,
688:                        NameCreationInfo creationInfo, Comment[] comments) {
689:                    super (name, creationInfo, comments);
690:                    this .basename = basename.intern();
691:                    this .index = index;
692:                }
693:
694:                public String getBaseName() {
695:                    return basename;
696:                }
697:
698:                public int getIndex() {
699:                    return index;
700:                }
701:            }
702:
703:            /**
704:             * temporary indexed ProgramElementName
705:             */
706:            private static class TempIndProgramElementName extends
707:                    IndProgramElementName {
708:                static final char SEPARATOR = '#';
709:
710:                TempIndProgramElementName(String basename, int index,
711:                        NameCreationInfo creationInfo) {
712:                    super (basename + SEPARATOR + index, basename, index,
713:                            creationInfo);
714:                }
715:
716:                TempIndProgramElementName(String basename, int index,
717:                        NameCreationInfo creationInfo, Comment[] comments) {
718:                    super (basename + SEPARATOR + index, basename, index,
719:                            creationInfo, comments);
720:                }
721:            }
722:
723:            /**
724:             * regular indexed ProgramElementName
725:             */
726:            private static class PermIndProgramElementName extends
727:                    IndProgramElementName {
728:                static final char SEPARATOR = '_';
729:
730:                PermIndProgramElementName(String basename, int index,
731:                        NameCreationInfo creationInfo) {
732:                    super (
733:                            basename
734:                                    + (index == 0 ? "" : SEPARATOR + "" + index),
735:                            basename, index, creationInfo);
736:                }
737:
738:                PermIndProgramElementName(String basename, int index,
739:                        NameCreationInfo creationInfo, Comment[] comments) {
740:                    super (
741:                            basename
742:                                    + (index == 0 ? "" : SEPARATOR + "" + index),
743:                            basename, index, creationInfo, comments);
744:                }
745:            }
746:
747:            /**
748:             * wrapper for global variables coming as a ListOfNamed
749:             */
750:            private static class GlobalsAsListOfNamed implements  Globals {
751:                private ListOfNamed globals;
752:
753:                public GlobalsAsListOfNamed(ListOfNamed globals) {
754:                    this .globals = globals;
755:                }
756:
757:                public IteratorOfProgramElementName iterator() {
758:                    return new AdapterOfIteratorOfNamed(globals.iterator());
759:                }
760:            }
761:
762:            /**
763:             * wrapper for global variables coming as a SetOfProgramVariable
764:             */
765:            private static class GlobalsAsSetOfProgramVariable implements 
766:                    Globals {
767:                private SetOfProgramVariable globals;
768:
769:                public GlobalsAsSetOfProgramVariable(
770:                        SetOfProgramVariable globals) {
771:                    this .globals = globals;
772:                }
773:
774:                public IteratorOfProgramElementName iterator() {
775:                    return new AdapterOfIteratorOfProgramVariable(globals
776:                            .iterator());
777:                }
778:            }
779:
780:            /**
781:             * adapter from IteratorOfNamed to IteratorOfProgramElementName
782:             */
783:            private static class AdapterOfIteratorOfNamed implements 
784:                    IteratorOfProgramElementName {
785:                private IteratorOfNamed it;
786:
787:                public AdapterOfIteratorOfNamed(IteratorOfNamed it) {
788:                    this .it = it;
789:                }
790:
791:                public boolean hasNext() {
792:                    return it.hasNext();
793:                }
794:
795:                public ProgramElementName next() {
796:                    return (ProgramElementName) (it.next().name());
797:                }
798:            }
799:
800:            /**
801:             * adapter from IteratorOfProgramVariable to IteratorOfProgramElementName
802:             */
803:            private static class AdapterOfIteratorOfProgramVariable implements 
804:                    IteratorOfProgramElementName {
805:                private IteratorOfProgramVariable it;
806:
807:                public AdapterOfIteratorOfProgramVariable(
808:                        IteratorOfProgramVariable it) {
809:                    this .it = it;
810:                }
811:
812:                public boolean hasNext() {
813:                    return it.hasNext();
814:                }
815:
816:                public ProgramElementName next() {
817:                    return it.next().getProgramElementName();
818:                }
819:            }
820:
821:            /**
822:             * a customized JavaASTWalker
823:             */
824:            private abstract static class CustomJavaASTWalker extends
825:                    JavaASTWalker {
826:                private ProgramElement declarationNode = null;
827:                private int declarationScopeDepth = -2;
828:                private int currentScopeDepth = -2;
829:
830:                CustomJavaASTWalker(ProgramElement program,
831:                        PosInProgram posOfDeclaration) {
832:                    super (program);
833:                    if (posOfDeclaration != null) {
834:                        declarationNode = PosInProgram.getProgramAt(
835:                                posOfDeclaration, program);
836:                    }
837:                }
838:
839:                protected void walk(ProgramElement node) {
840:                    //ignore ExecutionContext and ProgramMethod branches;
841:                    //ignore anything rooted at a depth less or equal than the depth
842:                    //of the scope containing the declaration (except for this
843:                    //"declaration scope" itself);
844:                    if (node instanceof  ExecutionContext
845:                            || node instanceof  ProgramMethod) {
846:                        return;
847:                    } else if (node instanceof  ScopeDefiningElement) {
848:                        currentScopeDepth = depth();
849:                    } else if (node == declarationNode) {
850:                        declarationScopeDepth = currentScopeDepth;
851:                    } else if (depth() <= declarationScopeDepth) {
852:                        return;
853:                    }
854:
855:                    super .walk(node);
856:                }
857:            }
858:
859:            /**
860:             * internal representation for global variables
861:             */
862:            protected static interface Globals {
863:                public IteratorOfProgramElementName iterator();
864:            }
865:
866:            /**
867:             * tuple of a basename and an index
868:             */
869:            protected static class BasenameAndIndex {
870:                public String basename;
871:                public int index;
872:            }
873:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.