ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
Chapter. Programs Operating on Trees.
Section. Binary Trees.
Subsection. Basic Operations and Predicates.
Permutations. Given binary trees t1 and t2 , the predicate t1 ∼ t2 holds if the trees t1 and t2 are permutations of each other.
Section. Applications of Trees.
Subsection. Heaps and Priority Queues.
Heaps.
We have
Maintaining the heap property. Define the function Heapify (t) such that
Building a heap. Define the function Brt2heap (t) such that
The enqueue operation. Define the function Enqueue (t,x) such that
The dequeue operation. Define the function Dequeue (t) such that