Source Code Cross Referenced for Update.java in  » Testing » KeY » de » uka » ilkd » key » rule » updatesimplifier » 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.updatesimplifier 
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:        package de.uka.ilkd.key.rule.updatesimplifier;
010:
011:        import java.util.HashMap;
012:        import java.util.HashSet;
013:
014:        import de.uka.ilkd.key.logic.Name;
015:        import de.uka.ilkd.key.logic.Term;
016:        import de.uka.ilkd.key.logic.op.*;
017:        import de.uka.ilkd.key.logic.sort.AbstractSort;
018:        import de.uka.ilkd.key.logic.sort.SetAsListOfSort;
019:        import de.uka.ilkd.key.logic.sort.SetOfSort;
020:        import de.uka.ilkd.key.logic.sort.Sort;
021:        import de.uka.ilkd.key.util.Debug;
022:
023:        /**
024:         * represents an update and is used as basis data structure for the
025:         * updatesimplifier. Currently this is only a naive default implementation.
026:         */
027:        public abstract class Update {
028:
029:            // just for unique handling of anonymous updates
030:            // it as to be taken care that this sort does not escape
031:            private static final Sort SPECIAL_SORT = new AbstractSort(new Name(
032:                    "special_sort")) {
033:                public SetOfSort extendsSorts() {
034:                    return SetAsListOfSort.EMPTY_SET;
035:                }
036:            };
037:
038:            /**
039:             * @author bubel
040:             */
041:            public static class UpdateInParts extends Update {
042:
043:                private final HashMap loc2assignmentPairs;
044:
045:                private final HashSet locationCache;
046:
047:                private final ArrayOfAssignmentPair pairs;
048:
049:                private SetOfQuantifiableVariable freeVars = null;
050:
051:                /**
052:                 * @param pairs
053:                 */
054:                public UpdateInParts(final ArrayOfAssignmentPair pairs) {
055:                    this .pairs = pairs;
056:                    loc2assignmentPairs = new HashMap();
057:                    this .locationCache = new HashSet();
058:
059:                    for (int i = 0; i < pairs.size(); i++) {
060:                        locationCache
061:                                .add(pairs.getAssignmentPair(i).location());
062:                    }
063:
064:                }
065:
066:                /*
067:                 * (non-Javadoc)
068:                 * 
069:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAllAssignmentPairs()
070:                 */
071:                public ArrayOfAssignmentPair getAllAssignmentPairs() {
072:                    return pairs;
073:                }
074:
075:                /*
076:                 * (non-Javadoc)
077:                 * 
078:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAssignmentPairs(de.uka.ilkd.key.logic.op.Operator)
079:                 */
080:                public ArrayOfAssignmentPair getAssignmentPairs(Location loc) {
081:                    if (!loc2assignmentPairs.containsKey(loc)) {
082:                        ListOfAssignmentPair result = SLListOfAssignmentPair.EMPTY_LIST;
083:                        for (int i = pairs.size() - 1; i >= 0; i--) {
084:                            AssignmentPair assignmentPair = pairs
085:                                    .getAssignmentPair(i);
086:                            final Location op = assignmentPair.location();
087:                            if (loc.mayBeAliasedBy(op)) {
088:                                result = result.prepend(assignmentPair);
089:                            }
090:                        }
091:
092:                        loc2assignmentPairs.put(loc, new ArrayOfAssignmentPair(
093:                                result.toArray()));
094:                    }
095:                    return (ArrayOfAssignmentPair) loc2assignmentPairs.get(loc);
096:                }
097:
098:                /*
099:                 * (non-Javadoc)
100:                 * 
101:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#hasLocation(de.uka.ilkd.key.logic.op.Operator)
102:                 */
103:                public boolean hasLocation(Location loc) {
104:                    return locationCache.contains(loc);
105:                }
106:
107:                /*
108:                 * (non-Javadoc)
109:                 * 
110:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#location(int)
111:                 */
112:                public Location location(int n) {
113:                    return pairs.getAssignmentPair(n).location();
114:                }
115:
116:                /*
117:                 * (non-Javadoc)
118:                 * 
119:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#locationCount()
120:                 */
121:                public int locationCount() {
122:                    return pairs.size();
123:                }
124:
125:                /* (non-Javadoc)
126:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#freeVars()
127:                 */
128:                public SetOfQuantifiableVariable freeVars() {
129:                    if (freeVars == null) {
130:                        freeVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
131:                        for (int i = 0; i != pairs.size(); ++i)
132:                            freeVars = freeVars.union(pairs
133:                                    .getAssignmentPair(i).freeVars());
134:                    }
135:                    return freeVars;
136:                }
137:
138:                /* (non-Javadoc)
139:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAssignmentPair(int)
140:                 */
141:                public AssignmentPair getAssignmentPair(int locPos) {
142:                    return pairs.getAssignmentPair(locPos);
143:                }
144:            }
145:
146:            private static class UpdateWithUpdateTerm extends Update {
147:
148:                private final HashMap loc2assignmentPairs;
149:
150:                private HashSet locationCache;
151:
152:                private final Term update;
153:
154:                private final IUpdateOperator updateOp;
155:
156:                private SetOfQuantifiableVariable freeVars = null;
157:
158:                public UpdateWithUpdateTerm(Term update) {
159:                    this .update = update;
160:                    this .updateOp = (IUpdateOperator) update.op();
161:                    this .loc2assignmentPairs = new HashMap();
162:
163:                    for (int i = 0; i < updateOp.locationCount(); i++) {
164:                        if (updateOp.location(i) == StarLocation.ALL)
165:                            Debug
166:                                    .fail("Anonymous update shall not be created using this "
167:                                            + "class. (at least as long no generalized terms are "
168:                                            + "supported)");
169:                    }
170:                }
171:
172:                /**
173:                 * @return
174:                 */
175:                public ArrayOfAssignmentPair getAllAssignmentPairs() {
176:                    final AssignmentPair[] result = new AssignmentPair[locationCount()];
177:                    for (int i = 0; i < locationCount(); i++) {
178:                        result[i] = getAssignmentPair(i);
179:                    }
180:                    return new ArrayOfAssignmentPair(result);
181:                }
182:
183:                public AssignmentPair getAssignmentPair(int locPos) {
184:                    if (updateOp instanceof  AnonymousUpdate)
185:                        return new AssignmentPairLazy(update, locPos);
186:                    else if (updateOp instanceof  QuanUpdateOperator)
187:                        return new QuanAssignmentPairLazy(update, locPos);
188:                    else
189:                        Debug.fail("Unknown update operator");
190:                    return null; // unreachable
191:                }
192:
193:                /**
194:                 * determines and returns all assignment pairs whose location part may 
195:                 * be an alias of <code>loc</code>
196:                 */
197:                public ArrayOfAssignmentPair getAssignmentPairs(Location loc) {
198:                    if (!loc2assignmentPairs.containsKey(loc)) {
199:                        ListOfAssignmentPair result = SLListOfAssignmentPair.EMPTY_LIST;
200:                        for (int i = updateOp.locationCount() - 1; i >= 0; i--) {
201:                            if (loc.mayBeAliasedBy(updateOp.location(i)))
202:                                result = result.prepend(getAssignmentPair(i));
203:                        }
204:
205:                        loc2assignmentPairs.put(loc, new ArrayOfAssignmentPair(
206:                                result.toArray()));
207:                    }
208:                    return (ArrayOfAssignmentPair) loc2assignmentPairs.get(loc);
209:                }
210:
211:                public boolean hasLocation(Location loc) {
212:                    if (locationCache == null) {
213:                        this .locationCache = new HashSet();
214:
215:                        for (int i = 0; i < updateOp.locationCount(); i++) {
216:                            locationCache.add(updateOp.location(i));
217:                        }
218:                    }
219:                    return locationCache.contains(loc);
220:                }
221:
222:                public Location location(int n) {
223:                    return updateOp.location(n);
224:                }
225:
226:                /**
227:                 * returns the number of locations
228:                 * 
229:                 * @return the number of locations as int
230:                 */
231:                public int locationCount() {
232:                    return updateOp.locationCount();
233:                }
234:
235:                /* (non-Javadoc)
236:                 * @see de.uka.ilkd.key.rule.updatesimplifier.Update#freeVars()
237:                 */
238:                public SetOfQuantifiableVariable freeVars() {
239:                    if (freeVars == null) {
240:                        if (update.sub(update.arity() - 1).freeVars().size() == 0) {
241:                            freeVars = update.freeVars();
242:                        } else {
243:                            freeVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
244:                            for (int i = 0; i != locationCount(); ++i)
245:                                freeVars = freeVars.union(getAssignmentPair(i)
246:                                        .freeVars());
247:                        }
248:                    }
249:                    return freeVars;
250:                }
251:            }
252:
253:            /**
254:             * creates an update representation out of the top level operator of the
255:             * given update term
256:             */
257:            public static Update createUpdate(AssignmentPair[] pairs) {
258:                return new UpdateInParts(new ArrayOfAssignmentPair(pairs));
259:            }
260:
261:            /**
262:             * creates an update representation out of the top level operator of the
263:             * given update term. If it is no update term an update with zero assignment 
264:             * pairs is returned (only for temporarly representations)
265:             */
266:            public static Update createUpdate(Term t) {
267:                if (t.op() instanceof  AnonymousUpdate) {
268:                    Term valueTerm = UpdateSimplifierTermFactory.DEFAULT
269:                            .getBasicTermFactory().createFunctionTerm(
270:                                    new RigidFunction(t.op().name(),
271:                                            SPECIAL_SORT, new Sort[0]));
272:                    AssignmentPair pair = new AssignmentPairImpl(
273:                            StarLocation.ALL, new Term[0], valueTerm);
274:                    return createUpdate(new AssignmentPair[] { pair });
275:                } else if (!(t.op() instanceof  IUpdateOperator)) {
276:                    return createUpdate(new AssignmentPair[0]);
277:                }
278:                return new UpdateWithUpdateTerm(t);
279:            }
280:
281:            /**
282:             * @return
283:             */
284:            public abstract ArrayOfAssignmentPair getAllAssignmentPairs();
285:
286:            /**
287:             * determines and returns all assignment pairs whose location part has the
288:             * same top level operator as the given one
289:             */
290:            public abstract ArrayOfAssignmentPair getAssignmentPairs(
291:                    Location loc);
292:
293:            /**
294:             * returns true if the given location is updated by this update
295:             * 
296:             * @param location
297:             *            the Operator specifying the location which is updated
298:             * @return true if location occurs on the left side of an assignment pair in
299:             *         this update
300:             */
301:            public abstract boolean hasLocation(Location loc);
302:
303:            /**
304:             * returns the n-th location operator
305:             * 
306:             * @param n
307:             *            an int specifying the position of the location operator to be
308:             *            retrieved
309:             * @return the n-tl location operator
310:             */
311:            public abstract Location location(int n);
312:
313:            /**
314:             * returns the number of locations
315:             * 
316:             * @return the number of locations as int
317:             */
318:            public abstract int locationCount();
319:
320:            /**
321:             * returns true if this update object describes an anonymous update
322:             */
323:            public boolean isAnonymousUpdate() {
324:                return hasLocation(StarLocation.ALL);
325:            }
326:
327:            /**
328:             * @return the set of quantifiable variables that turn up free in this
329:             *         update (when applying the update, it might happen that such
330:             *         variables have to be renaming to avoid collisions)
331:             */
332:            public abstract SetOfQuantifiableVariable freeVars();
333:
334:            public String toString() {
335:                StringBuffer result = new StringBuffer("{");
336:                ArrayOfAssignmentPair pairs = getAllAssignmentPairs();
337:                for (int i = 0; i < pairs.size(); i++) {
338:                    result.append(pairs.getAssignmentPair(i).toString());
339:                    if (i < pairs.size() - 1)
340:                        result.append(" || ");
341:                }
342:                result.append("}");
343:                return result.toString();
344:            }
345:
346:            // these classes are used to unify treatment of anonymous and 
347:            // normal updates. May become obsolete with generalized terms 
348:            public static class StarLocation extends NonRigidFunction implements 
349:                    Location {
350:
351:                // important "name" must be initialized before ALL!
352:                private final static Name name = new Name("*");
353:
354:                public final static StarLocation ALL = new StarLocation();
355:
356:                private StarLocation() {
357:                    super (name, SPECIAL_SORT, new Sort[0]);
358:                }
359:
360:                /* (non-Javadoc)
361:                 * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy(de.uka.ilkd.key.logic.op.Location)
362:                 */
363:                public boolean mayBeAliasedBy(Location loc) {
364:                    return false;
365:                }
366:
367:                /* (non-Javadoc)
368:                 * @see de.uka.ilkd.key.logic.op.Operator#name()
369:                 */
370:                public Name name() {
371:                    return name;
372:                }
373:
374:                /* (non-Javadoc)
375:                 * @see de.uka.ilkd.key.logic.op.Operator#validTopLevel(de.uka.ilkd.key.logic.Term)
376:                 */
377:                public boolean validTopLevel(Term term) {
378:                    return term.arity() == 0 && term.sort() != Sort.FORMULA;
379:                }
380:
381:                /* (non-Javadoc)
382:                 * @see de.uka.ilkd.key.logic.op.Operator#sort(de.uka.ilkd.key.logic.Term[])
383:                 */
384:                public Sort sort(Term[] term) {
385:                    return SPECIAL_SORT;
386:                }
387:
388:                /* (non-Javadoc)
389:                 * @see de.uka.ilkd.key.logic.op.Operator#arity()
390:                 */
391:                public int arity() {
392:                    return 0;
393:                }
394:
395:                /* (non-Javadoc)
396:                 * @see de.uka.ilkd.key.logic.op.Operator#isRigid(de.uka.ilkd.key.logic.Term)
397:                 */
398:                public boolean isRigid(Term term) {
399:                    return true;
400:                }
401:
402:            }
403:
404:            public abstract AssignmentPair getAssignmentPair(int locPos);
405:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.