Array list: find

Algorithmic problem: Linear sequence: find

Prerequisites: None.

Type of algorithm: loop

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

Abstract view

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

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

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

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

Induction basis

Abstract view: Set [math]\displaystyle{ 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]\displaystyle{ \Kappa }[/math] is found in the current array.
2. Otherwise, [math]\displaystyle{ p }[/math] is moved one step forward to the next array.

Implementation:

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

Correctness: Obvious.

Complexity

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

Proff: Obvious.