Algorithm Design Template Base on Temporal ADT

Design and Analysis of Computer Algorithms is a must of Computer Curricula. It covers many topics that group around several core themes. These themes range from data structures to complexity theory, but one very special theme is algorithmic design patterns, including greedy method, divide-and-conquer, dynamic programming, backtracking and branch-and-bound. Naturally, at the undergraduate level all listed design patterns are taught, learnt and comprehended by examples. But they can be semi-formalized as design templates, semi-specified by correctness conditions, and semi-formally verified, for example, by means of Manna - Pnueli proof-principles. Moreover, this approach can lead to new insights and better comprehension of the design patterns, specification and verification methods. In this paper we demonstrate an utility of the approach by study of backtracking and branch-and-bound design patterns. In particular, we present, specify and prove correctness of the unified template for these patterns. Our approach is based on a temporal abstract data type the que that unifies stack and queue discipline. We prove that every algorithm instantiated from the template is totally correct, if the input graph for traversing is finite, the boundary condition is monotone, and the decision condition is anti-monotone on sets of "visited" vertices.