Source Code Cross Referenced for TranslationVisitor.java in  » Testing » KeY » de » uka » ilkd » key » proof » decproc » translation » 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.decproc.translation 
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.decproc.translation;
012:
013:        import org.apache.log4j.Logger;
014:        import de.uka.ilkd.key.logic.Term;
015:        import de.uka.ilkd.key.logic.Visitor;
016:
017:        /** This class representing a visitor intended to be used for the translation of KeY <tt>Term</tt>s.
018:         * <p>
019:         * The translate a <tt>Term</tt>, a <tt>TranslationVisitor</tt> instance will be passed to either 
020:         * the <tt>execPostOrder</tt> or the <tt>execPreOrder</tt> method of the given <tt>Term</tt>. 
021:         * These methods then call the <tt>visit</tt> method of the passed <tt>TranslationVisitor</tt> 
022:         * recursively, with the appropriate subterms of the given <tt>Term</tt> as arguments
023:         *
024:         * @author akuwertz
025:         * @version 1.0,  12/10/2006
026:         */
027:
028:        public abstract class TranslationVisitor extends Visitor {
029:
030:            /* Additional fields */
031:
032:            /** The array of translation rules represented by exactly one instance of an  
033:             * <tt>IOperatorTranslation</tt> subclass per rule. */
034:            protected IOperatorTranslation[] translationRules = null;
035:
036:            /** A counter indicating the level in the AST of the top level <tt>Term</tt> on which the 
037:             * currently translated subterms occurs */
038:            private int level = -1;
039:
040:            /** A <tt>Logger</tt> for logging and debugging the translation process */
041:            protected static final Logger logger = Logger
042:                    .getLogger(TranslationVisitor.class.getName());
043:
044:            /** A short <tt>String</tt> identifying the implementing <tt>TranslationVisitor</tt> subclass
045:             * which has produced the current log statement */
046:            protected String loggingSubclass;
047:
048:            /* String constants for failures during translation process */
049:            private static final String nothingTranslatedException = "No translation has been initiated up to now!";
050:            protected static final String translationNotFinishedException = "The translation of the current Term has not finished yet!";
051:            protected static final String NoReuseStateException = "Previous translation didn't finish successfully or result has not been fetched yet!";
052:
053:            /* Public method implementation */
054:
055:            /** A factory method for returning an instance of a <tt>TranslationVisitor</tt> implementing
056:             * subclass. It therefore must be implemented in that subclass. 
057:             * <p>
058:             * This method intends the reuse of already created subclass instances.  Subclasses overriding
059:             * this method should therefore use the Singleton pattern, enabling time and memory savings.
060:             * <p>
061:             * To reuse <tt>TranslationVisitor</tt> instances, they have to be in a well-defined, resuable
062:             * state. To ensure this state, the <tt>isReusable</tt> should be called by an overriding
063:             * implementation.<br> 
064:             * To reset an instance to a reusable state, the <tt>reset</tt> method should be used
065:             * 
066:             * @return a <tt>TranslationVisitor</tt> instance
067:             * 
068:             * @see #isReusable()
069:             * @see #reset()
070:             */
071:            public synchronized static TranslationVisitor getInstance() {
072:                throw new UnsupportedOperationException();
073:            }
074:
075:            /** The visit method of this <tt>TranslationVisitor</tt>. Takes a KeY <tt>Term</tt> and tries
076:             * to translate it
077:             * <p>
078:             * Has to be implemented by a specific subclass    
079:             *  
080:             * @see de.uka.ilkd.key.logic.Visitor#visit(de.uka.ilkd.key.logic.Term)
081:             */
082:            abstract public void visit(Term t);
083:
084:            /** This method is intended to be called only by the <tt>execPostOrder</tt> method of
085:             * class <tt>de.uka.ilkd.key.logic.Term</tt>
086:             * 
087:             * @see de.uka.ilkd.key.logic.Visitor#subtreeEntered(de.uka.ilkd.key.logic.Term)
088:             */
089:            public final void subtreeEntered(Term subtreeRoot) {
090:                logger.info(logThis("->Subtree entered!"));
091:                if (level == -1) {
092:                    level = 1;
093:                } else {
094:                    level++;
095:                }
096:            }
097:
098:            /** This method is intended to be called only by the <tt>execPostOrder</tt> method of
099:             * class <tt>de.uka.ilkd.key.logic.Term</tt>
100:             * 
101:             * @see de.uka.ilkd.key.logic.Visitor#subtreeLeft(de.uka.ilkd.key.logic.Term)
102:             */
103:            public final void subtreeLeft(Term subtreeRoot) {
104:                logger.info(logThis("<-Subtree left!"));
105:                level--;
106:            }
107:
108:            /** Returns the result of the translation process and resets this <tt>TranslationVisitor</tt>
109:             * for reuse.
110:             * <p>
111:             * The result is actually fetched by calling the <tt>getResult</tt> method of the implementing
112:             * subclass.
113:             * <p>
114:             * After calling this method, this <tt>TranslationVisitor</tt> instance is in reusable state.
115:             * 
116:             * @return the <tt>Object</tt> resulting from current <tt>Term</tt> translation
117:             * 
118:             * @throws IllegalStateException if this method is called during an unfinished translation
119:             *                               process or before any translation was initiated
120:             * @see #getResult()                              
121:             */
122:            public final Object getTranslationResult() {
123:                // A positive level value indicates an unfinished translation
124:                if (level > 0)
125:                    throw new IllegalStateException(
126:                            translationNotFinishedException);
127:                // A negative level value indicates that no translation was initiated 
128:                if (level < 0)
129:                    throw new IllegalStateException(nothingTranslatedException);
130:
131:                level = -1; // Reset visitor for reuse
132:
133:                logger
134:                        .debug(logThis("Visitor state is reusable, fetching result from subclass..."));
135:                return getResult(); // Provide a hook for subclasses
136:            }
137:
138:            /** Resets this <tt>TranslationVisitor</tt> for reuse.<br>
139:             * After execution of this method, the state of this <tt>TranslationVisistor</tt> is equal
140:             * to that of a newly created <tt>TranslationVisitor</tt>
141:             */
142:            public void reset() {
143:                logger.info(logThis("Reseted visitor!"));
144:                level = -1;
145:            }
146:
147:            /* Protected (subclass) methods */
148:
149:            /** Sets the translation rules by converting <tt>rules</tt> to an 
150:             * <tt>IOperatorTranslation</tt> array
151:             *  
152:             * @param rules the rules to be set 
153:             */
154:            protected final void setTranslationRules(
155:                    ListOfIOperatorTranslation rules) {
156:                translationRules = rules.toArray();
157:            }
158:
159:            /** Returns true if this <tt>TranslationVisitor</tt> is ready for the next translation process
160:             * 
161:             * @return true if this <tt>TranslationVisitor</tt> is ready to be reused; otherwise false
162:             */
163:            protected boolean isReusable() {
164:                // A level value of -1 indicates that the previous translation process has completed
165:                return level == -1;
166:            }
167:
168:            /** This methods provides a hook for implementing subclasses to forward their translation
169:             * results.
170:             * <p>
171:             * It is intended to be called exclusively by the <tt>getTranslationResult</tt> method
172:             * <p>
173:             * After calling this method on a <tt>TranslationVisitor</tt> subclass instance, the instance
174:             * has to be in the reusable state
175:             * 
176:             * @return the translation result provided by an implementing subclass
177:             * 
178:             * @see #getTranslationResult()
179:             */
180:            abstract protected Object getResult();
181:
182:            /** Take a <tt>String</tt> which should be logged and adds a subclass identifying tag to it
183:             * 
184:             * @param toLog the <tt>String</tt> to be logged
185:             * @return the given <tt>String</tt> extended by a subclass tag 
186:             */
187:            protected final String logThis(String toLog) {
188:                return "(" + loggingSubclass + ") " + toLog;
189:            }
190:
191:        }
w__w__w___.___j___a_va__2___s_.___c__o_m___ | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.