Array list: number
Algorithmic problem: Linear sequence: number
Prerequisites:
Type of algorithm: loop
Auxiliary data:
- A pointer [math]\displaystyle{ p }[/math] of type "pointer to array list item of type [math]\displaystyle{ K }[/math]".
- A counter [math]\displaystyle{ c \in \mathbb{N}_0 }[/math].
Abstract view
Invariant: After [math]\displaystyle{ i \ge 0 }[/math] iterations:
- The pointer [math]\displaystyle{ p }[/math] points to the array list item at position [math]\displaystyle{ i+1 }[/math] (or is void if there is no such item).
- The value of is the sum of the values n of all array list items at positions [math]\displaystyle{ 1,...,i }[/math].
Variant: [math]\displaystyle{ p }[/math] is moved one step forward so as to point to the next array list item.
Break condition: It is [math]\displaystyle{ p= }[/math] void.
Induction basis
Abstract view: Initialize [math]\displaystyle{ p }[/math] so as to point to the first array list item.
Implementation:
- Set [math]\displaystyle{ p:=first }[/math].
- Set [math]\displaystyle{ c:=0 }[/math].
Proof: Nothing to show.
Induction step
Abstract view: Add the number of elements in the current array and then go forward.
Implementation:
- If void, terminate the algorithm and return the value of [math]\displaystyle{ c }[/math].
- Otherwise:
- Set [math]\displaystyle{ c:=c+p }[/math].n.
- Set [math]\displaystyle{ p:=p }[/math].next.
Correctness: Nothing to show.
Complexity
Statement: Linear in the length of the sequence in the worst case (for a fixed value of ).
Proof: Obvious.