Constructing tournament representations: An exercise in pointwise relational programming

Abstract

List or set comprehensions are a wonderful means to define nondeterministic or relational programs. Despite their beauty, comprehensions are somewhat underused in program calculation. The purpose of this paper is to remind the program-calculation community that comprehensions provide a convenient language for specifying and deriving nondeterministic programs in a pointwise manner. We illustrate the style of reasoning by re-solving the well-known problem of constructing tournament representations: Given a sequence x of integers, construct a heap whose inorder traversal is x itself.