Walter Guttmann - Relation-Algebraic Verification of Disjoint-Set Forests

fi:10856 - Fundamenta Informaticae, November 10, 2024, Volume 192, Issue 1
Relation-Algebraic Verification of Disjoint-Set ForestsArticle

Authors: Walter Guttmann

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


    Volume: Volume 192, Issue 1
    Published on: November 10, 2024
    Accepted on: July 9, 2024
    Submitted on: January 26, 2023
    Keywords: Computer Science - Logic in Computer Science,F.3.1,F.3.2

    Consultation statistics

    This page has been seen 13 times.
    This article's PDF has been downloaded 11 times.