Heap as array: descendItem

Algorithmic problem: Heap as array: descendItem

Prerequisites:

Type of algorithm: loop

Auxiliary data: A natural number [math]\displaystyle{ \ell }[/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 parent's key and its parent's keys of the current heap item [math]\displaystyle{ h }[/math] identified by [math]\displaystyle{ /ell }[/math] are smaller than the key [math]\displaystyle{ h.key }[/math].

Variant:

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

Break condition:

1. [math]\displaystyle{ (2* \ell \le n \Rightarrow h.key \le TheHeap[2* \ell ].key) \land (2* \ell +1 \le n \Rightarrow h.key \le TheHeap[2* \le +1].key) }[/math]

Induction basis

Abstract view:

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

Implementation:

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

Proof: Obvious.