Source Code Cross Referenced for ContextSkolemBuilder.java in  » Testing » KeY » de » uka » ilkd » key » rule » soundness » 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.rule.soundness 
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.rule.soundness;
012:
013:        import de.uka.ilkd.key.java.Services;
014:        import de.uka.ilkd.key.java.Statement;
015:        import de.uka.ilkd.key.java.StatementBlock;
016:        import de.uka.ilkd.key.java.abstraction.*;
017:        import de.uka.ilkd.key.java.declaration.Modifier;
018:        import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
019:        import de.uka.ilkd.key.java.declaration.VariableSpecification;
020:        import de.uka.ilkd.key.java.reference.ExecutionContext;
021:        import de.uka.ilkd.key.java.reference.TypeRef;
022:        import de.uka.ilkd.key.java.reference.VariableReference;
023:        import de.uka.ilkd.key.java.statement.*;
024:        import de.uka.ilkd.key.logic.*;
025:        import de.uka.ilkd.key.logic.op.*;
026:        import de.uka.ilkd.key.logic.sort.ProgramSVSort;
027:        import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
028:        import de.uka.ilkd.key.rule.inst.SVInstantiations;
029:        import de.uka.ilkd.key.util.ExtList;
030:
031:        /**
032:         * Replace context schema variables (..  ...) with nested method frames and try
033:         * blocks, together with a number of statement skolem symbols to
034:         * simulate code fragments.
035:         */
036:        public class ContextSkolemBuilder extends AbstractSkolemBuilder {
037:
038:            // Statement SV that are used to represent enclosing code
039:            private final Statement[] frameSVs;
040:
041:            // Variables that describe the try-frame
042:            private final Statement tryStatement;
043:            private ListOfSchemaVariable tryVariables = SLListOfSchemaVariable.EMPTY_LIST;
044:
045:            // Variables that describe the method frame
046:            private Statement resultStatement = null;
047:            private ListOfSchemaVariable resultVariables = null;
048:            private SVTypeInfo resultSVTypeInfo = null;
049:
050:            // The insertion point of the whole frame
051:            private ListOfInteger insertionPoint = SLListOfInteger.EMPTY_LIST;
052:
053:            public ContextSkolemBuilder(SkolemSet p_oriSkolemSet,
054:                    Services p_services) {
055:                super (p_oriSkolemSet, p_services);
056:
057:                frameSVs = createStatementSVs();
058:                tryStatement = createTryStatement();
059:            }
060:
061:            public IteratorOfSkolemSet build() {
062:                ListOfSkolemSet res = SLListOfSkolemSet.EMPTY_LIST;
063:
064:                IteratorOfKeYJavaType typeIt = getTypeCandidates();
065:                while (typeIt.hasNext()) {
066:                    setupFrame(typeIt.next());
067:                    res = res.append(createSkolemSet());
068:                    resetMethodFrame();
069:                }
070:
071:                return res.iterator();
072:            }
073:
074:            private SkolemSet createSkolemSet() {
075:                final PosInProgram pip = toPosInProgram(insertionPoint);
076:                final SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS
077:                        .add(pip, pip, createDummyExecutionContext(), // TODO: something with execution context
078:                                resultStatement);
079:
080:                SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
081:                        getServices(), svi, Constraint.BOTTOM, false, null,
082:                        true, false);
083:                getOriginalFormula().execPostOrder(srv);
084:
085:                SkolemSet res = getOriginalSkolemSet()
086:                        .setFormula(srv.getTerm()).addMissing(
087:                                resultVariables.iterator());
088:
089:                if (resultSVTypeInfo != null)
090:                    res = res.setSVTypeInfos(res.getSVTypeInfos().addInfo(
091:                            resultSVTypeInfo));
092:
093:                return res;
094:            }
095:
096:            private PosInProgram toPosInProgram(ListOfInteger p) {
097:                IteratorOfInteger it = p.iterator();
098:                PosInProgram res = PosInProgram.TOP;
099:
100:                while (it.hasNext())
101:                    res = res.down(it.next().intValue());
102:
103:                return res;
104:            }
105:
106:            private void addTryVariable(SchemaVariable p_var) {
107:                tryVariables = tryVariables.prepend(p_var);
108:            }
109:
110:            private void addResultVariable(SchemaVariable p_var) {
111:                resultVariables = resultVariables.prepend(p_var);
112:            }
113:
114:            /**
115:             * @return types that are possible result types of the method
116:             * frame to be created; <code>null</code> means that the method frame
117:             * should not have a result variable
118:             */
119:            private IteratorOfKeYJavaType getTypeCandidates() {
120:                final Type[] primitiveTypes = new Type[] {
121:                        PrimitiveType.JAVA_LONG,
122:                        //	    PrimitiveType.JAVA_DOUBLE,
123:                        PrimitiveType.JAVA_BOOLEAN };
124:
125:                ListOfKeYJavaType list = SLListOfKeYJavaType.EMPTY_LIST;
126:                int i;
127:
128:                for (i = 0; i != primitiveTypes.length; ++i)
129:                    list = list.prepend(getJavaInfo().getKeYJavaType(
130:                            primitiveTypes[i]));
131:
132:                // <code>null</code> (i.e. no result variable) is added as the
133:                // first possibility to consider (also see class <code>POBuilder</code>)
134:                list = list.prepend((KeYJavaType) null);
135:
136:                return list.iterator();
137:            }
138:
139:            /**
140:             * Create the try frame
141:             */
142:            private Try createTryStatement() {
143:                final Catch catchObj = createCatchBlock();
144:
145:                final ExtList tryBodyStmts = new ExtList();
146:                // an empty statement to mark the position of insertion
147:                tryBodyStmts.add(new EmptyStatement());
148:                tryBodyStmts.add(getFrameStatementSV(0));
149:
150:                addTryVariable((SchemaVariable) getFrameStatementSV(0));
151:
152:                final StatementBlock tryBody = new StatementBlock(tryBodyStmts);
153:                up(0);
154:                up(0);
155:
156:                return new Try(tryBody, new Branch[] { catchObj });
157:            }
158:
159:            /**
160:             * Create the catch block of the try block
161:             */
162:            private Catch createCatchBlock() {
163:                final ParameterDeclaration thDecl = createTryGuardVariable();
164:                final StatementBlock catchBody = new StatementBlock(
165:                        getFrameStatementSV(1));
166:
167:                addTryVariable((SchemaVariable) getFrameStatementSV(1));
168:
169:                return new Catch(thDecl, catchBody);
170:            }
171:
172:            /**
173:             * Create the guard variable of the catch leg of the try block.
174:             * @return a <code>ParameterDeclaration</code> of the variable
175:             */
176:            private ParameterDeclaration createTryGuardVariable() {
177:                final KeYJavaType thType = getJavaInfo().getTypeByClassName(
178:                        "java.lang.Throwable");
179:                final TypeRef thRef = new TypeRef(thType);
180:
181:                final ProgramElementName thName = createUniquePEName("frame_th");
182:                final SchemaVariable thVar = SchemaVariableFactory
183:                        .createProgramSV(thName, ProgramSVSort.VARIABLE, false);
184:                final VariableSpecification thSpec = new VariableSpecification(
185:                        (IProgramVariable) thVar, thType);
186:                final ParameterDeclaration thDecl = new ParameterDeclaration(
187:                        new Modifier[0], thRef, thSpec, false);
188:
189:                addTryVariable(thVar);
190:
191:                return thDecl;
192:            }
193:
194:            /**
195:             * Create the complete frame statement for a given result type
196:             */
197:            private void setupFrame(KeYJavaType p_resultType) {
198:                resultVariables = tryVariables;
199:
200:                final MethodFrame mfObj = createMethodFrame(p_resultType);
201:
202:                final ExtList topLevelStmts = new ExtList();
203:                topLevelStmts.add(mfObj);
204:                topLevelStmts.add(getFrameStatementSV(2));
205:
206:                addResultVariable((SchemaVariable) getFrameStatementSV(2));
207:
208:                resultStatement = new StatementBlock(topLevelStmts);
209:                up(0);
210:            }
211:
212:            /**
213:             * Create the method frame statement
214:             */
215:            private MethodFrame createMethodFrame(KeYJavaType p_resultType) {
216:                final IProgramVariable resVar = createResultVariable(p_resultType);
217:
218:                final StatementBlock mfBody = new StatementBlock(tryStatement);
219:                up(0);
220:
221:                final MethodFrame mfObj = new MethodFrame(resVar,
222:                        createDummyExecutionContext(), mfBody);
223:                up(p_resultType == null ? 1 : 2);
224:
225:                return mfObj;
226:            }
227:
228:            /**
229:             * Create the result variable of the method frame
230:             * @param p_resultType the type the variable should have, or
231:             * <code>null</code> if the method frame is not to be given a result
232:             * variable at all 
233:             * @return the result variable, or <code>null</code> for
234:             * <code>p_resultType==null</code>
235:             */
236:            private IProgramVariable createResultVariable(
237:                    KeYJavaType p_resultType) {
238:                if (p_resultType == null) {
239:                    resultSVTypeInfo = null;
240:                    return null;
241:                }
242:
243:                final IProgramVariable res = (IProgramVariable) SchemaVariableFactory
244:                        .createProgramSV(createUniquePEName("frame_res"),
245:                                ProgramSVSort.VARIABLE, false);
246:
247:                resultSVTypeInfo = new SVTypeInfo(((SchemaVariable) res),
248:                        p_resultType);
249:                addResultVariable((SchemaVariable) res);
250:
251:                return res;
252:            }
253:
254:            /**
255:             * HACK to create an execution context somehow
256:             */
257:            private ExecutionContext createDummyExecutionContext() {
258:                ProgramElementName refName = new ProgramElementName("ref");
259:                ProgramVariable refVar = new LocationVariable(refName,
260:                        getJavaInfo().getJavaLangObject());
261:                VariableReference ref = new VariableReference(refVar);
262:                ExecutionContext context = new ExecutionContext(new TypeRef(
263:                        getJavaInfo().getJavaLangObject()), ref);
264:                return context;
265:            }
266:
267:            private void resetMethodFrame() {
268:                insertionPoint = insertionPoint.tail().tail().tail();
269:            }
270:
271:            /**
272:             * @param p_num the number of the SV to return;
273:             * currently <code>p_num</code> has to be an element of [0, 3)
274:             * @return frame statement SV with number <code>p_num</code>
275:             */
276:            private Statement getFrameStatementSV(int p_num) {
277:                return frameSVs[p_num];
278:            }
279:
280:            /**
281:             * Setup frame SV
282:             */
283:            private Statement[] createStatementSVs() {
284:                int i = 3;
285:                final Statement[] res = new Statement[i];
286:
287:                while (i-- != 0) {
288:                    final ProgramElementName name = createUniquePEName("frame_s"
289:                            + i);
290:                    res[i] = (Statement) SchemaVariableFactory.createProgramSV(
291:                            name, ProgramSVSort.STATEMENT, false);
292:                }
293:
294:                return res;
295:            }
296:
297:            /**
298:             * Modify the <code>insertionPoint</code> by increasing the depth by one;
299:             * this means that the old frame is made a direct subtree of the new frame  
300:             */
301:            private void up(int p) {
302:                final Integer t = new Integer(p);
303:                insertionPoint = insertionPoint.prepend(t);
304:            }
305:
306:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.