Heap as array: ascendItem

Algorithmic problem: Heap as array: ascendItem

Prerequisites:

Type of algorithm: loop

Auxiliary data:

1. A natural number [math]\displaystyle{ \ell }[/math] denoting a position within the heap.
2. A pointer [math]\displaystyle{ h }[/math] of type heap item.
3. A natural number [math]\displaystyle{ p }[/math] denoting a position within the heap.

Abstract view

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

1. [math]\displaystyle{ 1\le \ell \le n }[/math].
2. The left and right child's key and their children's keys of the current heap item [math]\displaystyle{ h }[/math] identified by [math]\displaystyle{ \ell }[/math] are bigger than the key [math]\displaystyle{ h.key }[/math].

Variant:

1. [math]\displaystyle{ \ell }[/math] decreases each step and points to a valid position within the heap that is at a higher level than before.

Break condition:

1. [math]\displaystyle{ \ell = 1 }[/math] or [math]\displaystyle{ TheHeap[\lfloor \ell /2 \rfloor ].key \le TheHeap[\ell].key }[/math]

Induction basis

Abstract view:

1. Set [math]\displaystyle{ \ell }[/math] to the positions of the heap item to be ascended.

Implementation:

1. [math]\displaystyle{ \ell := Positions[ID] }[/math]

Proof: Obvious: