de.uka.ilkd.key.logic

Interface PIOPathIterator

All Superinterfaces:

IntIterator

All Known Implementing Classes:

PosInOccurrence.PIOPathIteratorImpl

public interface PIOPathIterator
extends IntIterator

This interface represents an iterator, iterating the nodes on the path between the root of a term and a position within the term, given by a PosInOccurrence-object

Method Summary

Modifier and Type	Method and Description
int	getChild()
PosInOccurrence	getPosInOccurrence()
Term	getSubTerm()
int	next()

Methods inherited from interface de.uka.ilkd.key.logic.IntIterator

hasNext

Method Detail

next

int next()

Specified by:

next in interface IntIterator

Returns:

the number of the next child on the path, or -1 if no further child exists

getPosInOccurrence

PosInOccurrence getPosInOccurrence()

Returns:

the current position within the term (i.e. corresponding to the latest next()-call)

getSubTerm

Term getSubTerm()

Returns:

the current subterm this object points to (i.e. corresponding to the latest next()-call); this method satisfies getPosInOccurrence().subTerm()==getSubTerm()

getChild

int getChild()

Returns:

the number of the next child on the path, or -1 if no further child exists (this is the number that was also returned by the last call of next())