Relation-Algebraic Verification of Disjoint-Set Forests

Article type: Research Article

Authors: Guttmann, Walter^{; *}

Affiliations: Department of Computer Science and Software Engineering, University of Canterbury, Christchurch, New Zealand. walter.guttmann@canterbury.ac.nz

Correspondence: [*] Address for correspondence: Department of Computer Science and Software Engineering, University of Canterbury, Christchurch, New Zealand.

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].

Keywords: arrays, Kleene algebras, path compression, program verification, relation algebras, union-find

DOI: 10.3233/FI-242189

Journal: Fundamenta Informaticae, vol. 192, no. 1, pp. 77-120, 2024