Array list: number

Algorithmic problem: Ordered sequence: number

Prerequisites:

Type of algorithm: loop

Auxiliary data:

1. A pointer $p$ of type "pointer to array list item of type $K$".
2. A counter $c\in {\mathbb{N}}_0$.

Abstract view

Invariant: After $i\ge 0$ iterations:

1. The pointer $p$ points to the array list item at position $i+1$ (or is void if there is no such item).
2. The value of $c$ is the sum of the values n of all array list items at positions $1,...,i$.

Variant: $p$ is moved one step forward so as to point to the next array list item.

Break condition: It is $p=$ void.

Induction basis

Abstract view: Initialize $p$ so as to point to the first array list item.

Implementation:

1. Set $p:=$first.
2. Set $c:=0$.

Proof: Nothing to show.

Induction step

Abstract view: Add the number of elements in the current array and then go forward.

Implementation:

1. If $p=$void, terminate the algorithm and return the value of $c$.
2. Otherwise:
   1. Set $c:=c+p$.n.
   2. Set $p:=p$.next.

Correctness: Nothing to show.

Complexity

Statement: Linear in the length of the sequence in the worst case (if the arrays of all array list items have identical lengths).

Proof: Obvious.