Source Code Cross Referenced for PosInOccurrence.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:        //
009:        //
010:
011:        package de.uka.ilkd.key.logic;
012:
013:        import de.uka.ilkd.key.logic.op.Metavariable;
014:        import de.uka.ilkd.key.util.Debug;
015:
016:        /**
017:         * This class describes a position in an occurrence of a term. A
018:         * ConstrainedFormula and a PosInTerm determine an object of this 
019:         * class exactly. 
020:         */
021:        public class PosInOccurrence {
022:
023:            public static PosInOccurrence findInSequent(Sequent seq,
024:                    int formulaNumber, PosInTerm pos) {
025:                return new PosInOccurrence(seq.getFormulabyNr(formulaNumber),
026:                        pos, seq.numberInAntec(formulaNumber));
027:            }
028:
029:            /**
030:             * the constrained formula the pos in occurrence describes
031:             */
032:            private final ConstrainedFormula cfma;
033:
034:            private final int hashCode;
035:            /**
036:             * is true iff the position is in the antecedent of a sequent. 
037:             */
038:            private final boolean inAntec;
039:
040:            private final PosInTerm metaPosInTerm;
041:
042:            // Descend into metavariables instantiations
043:            private final Term metaTerm;
044:
045:            /** the position in cfma.formula() */
046:            private final PosInTerm posInTerm;
047:
048:            /**
049:             * The subterm this object points to, or <code>null</code>
050:             */
051:            private Term subTermCache = null;
052:
053:            public PosInOccurrence(ConstrainedFormula cfma,
054:                    PosInTerm posInTerm, boolean inAntec) {
055:                this (cfma, posInTerm, null, null, inAntec);
056:            }
057:
058:            private PosInOccurrence(ConstrainedFormula cfma,
059:                    PosInTerm posInTerm, Term metaTerm,
060:                    PosInTerm metaPosInTerm, boolean inAntec) {
061:                this .inAntec = inAntec;
062:                this .cfma = cfma;
063:                this .posInTerm = posInTerm;
064:                this .metaTerm = metaTerm;
065:                this .metaPosInTerm = metaPosInTerm;
066:                this .hashCode = computeHash();
067:            }
068:
069:            private int computeHash() {
070:                int res = constrainedFormula().hashCode() * 13
071:                        + posInTerm().hashCode();
072:                if (termBelowMetavariable() != null)
073:                    res += termBelowMetavariable().hashCode() * 13
074:                            + posInTermBelowMetavariable().hashCode();
075:                return res;
076:            }
077:
078:            /**
079:             * returns the ConstrainedFormula that determines the occurrence of
080:             * this PosInOccurrence 
081:             */
082:            public ConstrainedFormula constrainedFormula() {
083:                return cfma;
084:            }
085:
086:            /**
087:             * @return Depth of the represented position within a formula; top-level
088:             *         positions (<code>isTopLevel()</code> have depth zero
089:             */
090:            public int depth() {
091:                int res = posInTerm().depth();
092:
093:                if (termBelowMetavariable() != null)
094:                    res += posInTermBelowMetavariable().depth();
095:
096:                return res;
097:            }
098:
099:            /**
100:             * creates a new PosInOccurrence that has exactly the same state as this
101:             * object except the PosInTerm is new and walked down the specified
102:             * subterm, as specified in method down of 
103:             * {@link de.uka.ilkd.key.logic.PosInTerm}.
104:             */
105:            public PosInOccurrence down(int i) {
106:                if (metaTerm == null)
107:                    return new PosInOccurrence(cfma, posInTerm.down(i), inAntec);
108:                else
109:                    return new PosInOccurrence(cfma, posInTerm, metaTerm,
110:                            metaPosInTerm.down(i), inAntec);
111:            }
112:
113:            /** 
114:             * compares this PosInOccurrence with another PosInOccurrence
115:             * and returns true if both describe the same occurrence 
116:             */
117:            public boolean eqEquals(Object obj) {
118:                if (!(obj instanceof  PosInOccurrence)) {
119:                    return false;
120:                }
121:                final PosInOccurrence cmp = (PosInOccurrence) obj;
122:
123:                if (!constrainedFormula().equals(cmp.constrainedFormula())) {
124:                    return false;
125:                }
126:
127:                return equalsHelp(cmp);
128:            }
129:
130:            /**
131:             * Contrary to <code>eqEquals</code>, this method returns true only for pio
132:             * objects that point to the same (identical) formula
133:             * @param obj
134:             * @return
135:             */
136:            public boolean equals(Object obj) {
137:                if (!(obj instanceof  PosInOccurrence)) {
138:                    return false;
139:                }
140:                final PosInOccurrence cmp = (PosInOccurrence) obj;
141:
142:                // NB: the class <code>NonDuplicateAppFeature</code> depends on the usage
143:                // of <code>!=</code> in this condition
144:                if (constrainedFormula() != cmp.constrainedFormula()) {
145:                    return false;
146:                }
147:
148:                return equalsHelp(cmp);
149:            }
150:
151:            private boolean equalsHelp(final PosInOccurrence cmp) {
152:                if (isInAntec() == cmp.isInAntec()) {
153:                    if (!posInTerm().equals(cmp.posInTerm()))
154:                        return false;
155:
156:                    if (termBelowMetavariable() == null)
157:                        return cmp.termBelowMetavariable() == null;
158:                    else
159:                        return termBelowMetavariable().equals(
160:                                cmp.termBelowMetavariable())
161:                                && posInTermBelowMetavariable().equals(
162:                                        cmp.posInTermBelowMetavariable());
163:                }
164:                return false;
165:            }
166:
167:            /**
168:             * @return the number/index of the deepest subterm that this
169:             *         <code>PosInOccurrence</code> points to. If the position is
170:             *         top-level, the result will be <code>-1</code>
171:             */
172:            public int getIndex() {
173:                if (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL)
174:                    return posInTerm.getIndex();
175:                return metaPosInTerm.getIndex();
176:            }
177:
178:            public int hashCode() {
179:                return hashCode;
180:            }
181:
182:            /**
183:             * returns true iff the occurrence is in the
184:             * antecedent of a sequent. 
185:             */
186:            public boolean isInAntec() {
187:                return inAntec;
188:            }
189:
190:            public boolean isTopLevel() {
191:                return posInTerm == PosInTerm.TOP_LEVEL
192:                        && (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL);
193:            }
194:
195:            /**
196:             * List all subterms between the root and the position this
197:             * objects points to; the first term is the whole term
198:             * <code>constrainedFormula().formula()</code>, the last one
199:             * <code>subTerm()</code>
200:             * @return an iterator that walks from the root of the term to the
201:             * position this <code>PosInOccurrence</code>-object points to
202:             */
203:            public PIOPathIterator iterator() {
204:                return new PIOPathIteratorImpl();
205:            }
206:
207:            /**
208:             * The usage of this method is strongly discouraged, use 
209:             * {@link PosInOccurrence#iterator} instead.     
210:             * describes the exact occurence of the refered term inside 
211:             * {@link ConstrainedFormula#formula()} 
212:             * @returns the position in the formula of the ConstrainedFormula of
213:             * this PosInOccurrence. 
214:             */
215:            public PosInTerm posInTerm() {
216:                return posInTerm;
217:            }
218:
219:            /**
220:             *  The usage of this method is strongly discouraged, use 
221:             * {@link PosInOccurrence#iterator} instead.    
222:             */
223:            public PosInTerm posInTermBelowMetavariable() {
224:                return metaPosInTerm;
225:            }
226:
227:            /**
228:             * Replace the formula this object points to with the new formula given
229:             * 
230:             * @param p_newFormula
231:             *                the new formula
232:             * @return a <code>PosInOccurrence</code> object that points to the same
233:             *         position within the formula <code>p_newFormula</code> as this
234:             *         object does within the formula <code>constrainedFormula()</code>.
235:             *         It is not tested whether this position exists within <code>p_newFormula</code>
236:             */
237:            public PosInOccurrence replaceConstrainedFormula(
238:                    ConstrainedFormula p_newFormula) {
239:                final PIOPathIterator it = iterator();
240:                Term newTerm = p_newFormula.formula();
241:                PosInTerm newPosInTerm = PosInTerm.TOP_LEVEL;
242:                int depth = 0;
243:
244:                while (true) {
245:                    final int subNr = it.next();
246:
247:                    if (newTerm.op() instanceof  Metavariable
248:                            && depth == posInTerm().depth()) {
249:                        // It is necessary to insert a term below the metavariable,
250:                        // as the iterator still holds further elements
251:
252:                        return new PosInOccurrence(p_newFormula, posInTerm(),
253:                                termBelowMetavariable(),
254:                                posInTermBelowMetavariable(), inAntec);
255:                    }
256:
257:                    if (subNr == -1)
258:                        break;
259:
260:                    newPosInTerm = newPosInTerm.down(subNr);
261:                    newTerm = newTerm.sub(subNr);
262:                    ++depth;
263:                }
264:
265:                return new PosInOccurrence(p_newFormula, newPosInTerm, inAntec);
266:            }
267:
268:            /**
269:             * If "this" points to a metavariable, a term can be inserted at
270:             * this position, allowing to walk down the term further "inside"
271:             * the metavariable.
272:             */
273:            public PosInOccurrence setTermBelowMetavariable(Term p_metaTerm) {
274:                if (Debug.ENABLE_ASSERTION) {
275:                    Debug
276:                            .assertTrue(
277:                                    metaTerm == null
278:                                            && (constrainedFormula().formula()
279:                                                    .subAt(posInTerm).op() instanceof  Metavariable)
280:                                            && p_metaTerm.sort().extendsTrans(
281:                                                    constrainedFormula()
282:                                                            .formula().subAt(
283:                                                                    posInTerm)
284:                                                            .sort()),
285:                                    "Illegal position (no metavariable) or incompatible sorts");
286:                }
287:
288:                return new PosInOccurrence(cfma, posInTerm, p_metaTerm,
289:                        PosInTerm.TOP_LEVEL, inAntec);
290:            }
291:
292:            /**
293:             * returns the subterm this object points to
294:             */
295:            public Term subTerm() {
296:                if (subTermCache == null) {
297:                    if (metaTerm == null)
298:                        subTermCache = constrainedFormula().formula().subAt(
299:                                posInTerm);
300:                    else
301:                        subTermCache = metaTerm.subAt(metaPosInTerm);
302:                }
303:                return subTermCache;
304:            }
305:
306:            /** The usage of this method is strongly discouraged, use 
307:             * {@link PosInOccurrence#iterator} instead if possible.
308:             */
309:            public Term termBelowMetavariable() {
310:                return metaTerm;
311:            }
312:
313:            /**
314:             * Ascend to the top node of the formula this object points to 
315:             */
316:            public PosInOccurrence topLevel() {
317:                if (isTopLevel()) {
318:                    return this ;
319:                }
320:                return new PosInOccurrence(cfma, PosInTerm.TOP_LEVEL, inAntec);
321:            }
322:
323:            /** toString */
324:            public String toString() {
325:                String res = "Term " + posInTerm() + " of "
326:                        + constrainedFormula();
327:                if (termBelowMetavariable() != null)
328:                    res += " / Term " + posInTermBelowMetavariable() + " of "
329:                            + termBelowMetavariable();
330:                return res;
331:                //            formulaNumberInSequent()+" th formula";
332:
333:            }
334:
335:            /**
336:             * Ascend to the parent node
337:             */
338:            public PosInOccurrence up() {
339:                assert !isTopLevel() : "not possible to go up from top level position";
340:                if (metaTerm == null || metaPosInTerm == PosInTerm.TOP_LEVEL)
341:                    return new PosInOccurrence(cfma, posInTerm.up(), inAntec);
342:                else
343:                    return new PosInOccurrence(cfma, posInTerm, metaTerm,
344:                            metaPosInTerm.up(), inAntec);
345:            }
346:
347:            private class PIOPathIteratorImpl implements  PIOPathIterator {
348:                boolean belowMetavariable = false;
349:                int child;
350:                int count = 0;
351:                IntIterator currentPathIt;
352:                Term currentSubTerm = null;
353:
354:                private PIOPathIteratorImpl() {
355:                    currentPathIt = posInTerm().iterator();
356:                }
357:
358:                private PosInTerm firstN(PosInTerm p_pit, int p_n) {
359:                    IntIterator it = p_pit.iterator();
360:                    PosInTerm res = PosInTerm.TOP_LEVEL;
361:
362:                    while (p_n-- != 0)
363:                        res = res.down(it.next());
364:
365:                    return res;
366:                }
367:
368:                /**
369:                 * @return the number of the next child on the path, or
370:                 * <code>-1</code> if no further child exists (this is the number
371:                 * that was also returned by the last call of <code>next()</code>)
372:                 */
373:                public int getChild() {
374:                    return child;
375:                }
376:
377:                /**
378:                 * @return the current position within the term
379:                 * (i.e. corresponding to the latest <code>next()</code>-call)
380:                 */
381:                public PosInOccurrence getPosInOccurrence() {
382:                    // the object is created only now to make the method
383:                    // <code>next()</code> faster
384:
385:                    final PosInOccurrence pio;
386:                    if (belowMetavariable) {
387:                        pio = new PosInOccurrence(cfma, posInTerm, metaTerm,
388:                                firstN(metaPosInTerm, count - posInTerm.depth()
389:                                        - 1), inAntec);
390:                    } else {
391:                        pio = new PosInOccurrence(cfma, firstN(posInTerm,
392:                                count - 1), inAntec);
393:                    }
394:
395:                    return pio;
396:                }
397:
398:                /**
399:                 * @return the current subterm this object points to
400:                 * (i.e. corresponding to the latest <code>next()</code>-call);
401:                 * this method satisfies
402:                 * <code>getPosInOccurrence().subTerm()==getSubTerm()</code>
403:                 */
404:                public Term getSubTerm() {
405:                    return currentSubTerm;
406:                }
407:
408:                public boolean hasNext() {
409:                    return currentPathIt != null;
410:                }
411:
412:                /**
413:                 * @return the number of the next child on the path, or
414:                 * <code>-1</code> if no further child exists
415:                 */
416:                public int next() {
417:                    int res;
418:
419:                    if (currentSubTerm == null)
420:                        currentSubTerm = cfma.formula();
421:                    else
422:                        currentSubTerm = currentSubTerm.sub(child);
423:
424:                    if (currentPathIt.hasNext())
425:                        res = currentPathIt.next();
426:                    else if (!belowMetavariable
427:                            && termBelowMetavariable() != null) {
428:                        belowMetavariable = true;
429:                        currentPathIt = posInTermBelowMetavariable().iterator();
430:                        currentSubTerm = termBelowMetavariable();
431:
432:                        if (currentPathIt.hasNext())
433:                            res = currentPathIt.next();
434:                        else {
435:                            res = -1;
436:                            currentPathIt = null;
437:                        }
438:                    } else {
439:                        res = -1;
440:                        currentPathIt = null;
441:                    }
442:
443:                    child = res;
444:                    ++count;
445:                    return res;
446:                }
447:            }
448:
449:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.