Array list: insert at position
Algorithmic problem: Ordered sequence: insert at position
Type of algorithm: loop
Auxiliary data:
- A natural number sum
, which contains the total number of all elements seen so far in the visited arrays. - Two pointers,
and , of type "pointer to array list item of type ".
Abstract view
Invariant:After
- The pointer
points to the array at position in the array list. - It is sum
, where is the value of the component n of the array list item at position .
Variant: The pointer
Break condition: It is sum
Induction basis
Abstract view: Set
Implementation: Obvious.
Proof: Nothing to show.
Induction step
Abstract view: If the position
Implementation:
- If
void, terminate the algorithm and return false. - If sum
:- Set sum
sum . - Set
.next.
- Set sum
- Otherwise:
- If
:- Create a new array list item and let
point to this new list item. - Set
.next .next. - Set
.next . - For
, set and void. - Set
and, afterwards, .
- Create a new array list item and let
- If
sum :- Set
sum . - Set
.
- Set
- Otherwise, set
sum . - For
(in this order), set . - Set
.
- If
- Return true.
Correctness: Note that, in an implementation of Ordered sequence: insert at position, we may assume
Complexity
Statement: Linear in the length of the sequence in the worst case.
Proof: Obvious.