Distributed maximum maintenance on hierarchically divided graphs
P. J. A. Lentfert, S. Doaitse Swierstra · Formal Aspects of Computing · 1993
Abstract The design and verification of distributed and concurrent algorithms is highly complex, and thus error-prone. It is our experience that the intertwined use of an informal description as well as a formal method in designing and studying an algorithm, is a fruitful one. The advantage of the informal description is the ease with which algorithms can be produced, studied and discussed. In contrast with formal methods however, errors are easily made in informal arguments about programs that seem to be correct, but in fact are not. In this paper we use an informal argument, carefully augmented with the use of the UNITY formalism, in the design of a distributed algorithm for maintaining the maximum value of a bag of frequently changing integers on a hierarchically divided network. The resulting algorithm is obtained by first designing an abstract algorithm on a virtual datastructure. Next, the abstract algorithm is transformed into the distributed algorithm.