01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic;
12:
13: /**
14: * This interface represents an iterator, iterating the nodes on the
15: * path between the root of a term and a position within the term,
16: * given by a <code>PosInOccurrence</code>-object
17: */
18: public interface PIOPathIterator extends IntIterator {
19:
20: /**
21: * @return the number of the next child on the path, or
22: * <code>-1</code> if no further child exists
23: */
24: int next();
25:
26: // The following methods may only be called after having called
27: // <code>next()</code> at least once
28:
29: /**
30: * @return the current position within the term
31: * (i.e. corresponding to the latest <code>next()</code>-call)
32: */
33: PosInOccurrence getPosInOccurrence();
34:
35: /**
36: * @return the current subterm this object points to
37: * (i.e. corresponding to the latest <code>next()</code>-call);
38: * this method satisfies
39: * <code>getPosInOccurrence().subTerm()==getSubTerm()</code>
40: */
41: Term getSubTerm();
42:
43: /**
44: * @return the number of the next child on the path, or
45: * <code>-1</code> if no further child exists (this is the number
46: * that was also returned by the last call of <code>next()</code>)
47: */
48: int getChild();
49:
50: }
|