Verification of the Garsia–Wachs algorithm in Dafny

The Garsia–Wachs algorithm is an algorithm for finding a leaf-labeledbinary tree whose leaf sequence exactly matches the input weight sequence and whosecost is as small as possible, where the cost is the sum of the weights labeling the leavesmultiplied by their levels. The algorithm, along with a proof of correctness due toKingston, is presented in Knuth’s The Art of Computer Programming, Vol. 3. Thealgorithm comes in two versions, the naive and the optimized. Both versionshave quadratic time complexity, but the optimized version can be fine-tunedwith a suitable data structure to yield an O(n log n)-time algorithm. I implement andverify a variant of each version of the algorithm in the verification-aware programminglanguage Dafny. Unlike all previous presentations of the algorithm, these variantsconstruct the desired optimum tree directly, without detour through a “nonalphabetic”tree whose leaf sequence is a rearrangement of the input sequence.