Array list: find

Algorithmic problem: Ordered sequence: find

Prerequisites: None.

Type of algorithm: loop

Auxiliary data: A pointer [math]p[/math] of type "pointer to list item of array lists of component type [math]\Kappa[/math]".

Abstract view

Invariant: After [math]i \ge 0[/math] iterations:

1. The pointer [math]p[/math] points to the list item at position [math]i + 1[/math] (or is void if no such item exists).
2. The first [math]i[/math] arrays in the list do not contain [math]\Kappa[/math].

Variant: The pointer [math]p[/math] is moved one step forward to the next array list item.

Break condition: Either [math]p=[/math]void or, otherwise, [math]\Kappa \in \{p.A[1], \ldots, p.A[p.n]\}[/math].

Induction basis

Abstract view: Set [math]p:=[/math] first.

Implementation: Obvious.

Proof: Nothing to show.

Induction step

Abstract view:

1. Terminate the algorithm if the end of the list is reached or, otherwise, if [math]\Kappa[/math] is found in the current array.
2. Otherwise, [math]p[/math] is moved one step forward to the next array.

Implementation:

1. If [math]p=[/math]void, terminate the algorithm and return false.
2. Otherwise, if [math]p.A[j] = \Kappa[/math] for some [math]j \in \{1, \ldots, p.n\}[/math], terminate the algorithms and return true.
3. Set [math]p:=p.next[/math].

Correctness: Obvious.

Complexity

Statement: Linear in the length of the sequence in the worst case.

Proff: Obvious.