de.uka.ilkd.key.symbolic_execution

Class ExecutionNodePreorderIterator

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodePreorderIterator

public class ExecutionNodePreorderIterator
extends java.lang.Object

Iterates preorder over the whole sub tree of a given IExecutionNode.

Instances of this class should always be used instead of recursive method calls because they cause StackOverflowErrors even in small programs.

Attention: The iteration process does not take care of changes in the model. If the containment hierarchy changes during iteration it is possible that elements are left or visited multiple times. For this reason it is forbidden to change the model during iteration. But the developer has to take care about it.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private IExecutionNode<?>	next The next element or null if no more elements exists.
private IExecutionNode<?>	start The element at that the iteration has started used as end condition to make sure that only over the subtree of the element is iterated.

Constructor Summary

Constructors

Constructor and Description
ExecutionNodePreorderIterator(IExecutionNode<?> start) Constructor.

Method Summary

Modifier and Type	Method and Description
protected IExecutionNode<?>	getNextOnParent(IExecutionNode<?> node) Returns the next element to select if all children of the given IExecutionNode are visited.
boolean	hasNext() Checks if more elements are available.
IExecutionNode<?>	next() Returns the next IExecutionNode in the containment hierarchy.
protected void	updateNext() Computes the next element and updates next().

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

start

private IExecutionNode<?> start

The element at that the iteration has started used as end condition to make sure that only over the subtree of the element is iterated.

next

private IExecutionNode<?> next

The next element or null if no more elements exists.

Constructor Detail

ExecutionNodePreorderIterator

public ExecutionNodePreorderIterator(IExecutionNode<?> start)

Constructor.

Parameters:

start - The IExecutionNode to iterate over its sub tree.

Method Detail

hasNext

public boolean hasNext()

Checks if more elements are available.

Returns:

true has more elements, false has not more elements.

next

public IExecutionNode<?> next()

Returns the next IExecutionNode in the containment hierarchy.

Returns:

The next IExecutionNode.

updateNext

protected void updateNext()

Computes the next element and updates next().

getNextOnParent

protected IExecutionNode<?> getNextOnParent(IExecutionNode<?> node)

Returns the next element to select if all children of the given IExecutionNode are visited.

Parameters:

node - The visited IExecutionNode.

Returns:

The next IExecutionNode to visit.