MOQA min-max heapify: A randomness preserving algorithm

MOQA is a high-level data structuring language, designed to allow for modular static timing analysis [1,2,3]. In essence, MOQA allows the programmer to determine the average running time of a broad class of programmes directly from the code in a (semi-)automated way. The modularity property brings a strong advantage for the programmer. The capacity to combine parts of code, where the average-time is simply the sum of the times of the parts, is a very helpful advantage in static analysis, something which is not available in current languages. Modularity also improves precision of average-case analysis, supporting the determination of accurate estimates on the average number of basic operations ofMOQA programs. The mathematical theory underpinning this approach is that of random structures and their preservation. Applying any MOQA operation to all elements of a random structure results in an output isomorphic to one or more random structures, which is the key to systematic timing. Here we introduce the approach in a self contained way and provide a MOQA version of the well-known algorithm of Min-Max heapify, constructed with the MOQA product operation. We demonstrate the "randomness preservation" property of the algorithm and illustrate the applicability of our method by deriving the exact average time of the algorithm.