Relation-Algebraic Verification of Disjoint-Set Forests

TL;DR

This paper demonstrates how relation algebras can be used to verify the correctness of array-based disjoint-set forest algorithms, with formal proofs in Isabelle/HOL.

Contribution

It introduces a relation-algebraic semantics for array operations and applies it to verify disjoint-set forest algorithms with advanced path compression techniques.

Findings

Verified correctness of union-by-rank disjoint-set forests

Formal proofs of array operations in Isabelle/HOL

Unified relation-algebraic framework for program verification

Abstract

This paper studies how to use relation algebras, which are useful for high-level specification and verification, for proving the correctness of lower-level array-based implementations of algorithms. We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in computation models supporting while-programs. As a result, relation algebras can be used for verifying programs with associative arrays. We verify the correctness of an array-based implementation of disjoint-set forests using the union-by-rank strategy and find operations with path compression, path splitting and path halving. All results are formally proved in Isabelle/HOL. This paper is an extended version of [1].