Relation-Algebraic Verification of Disjoint-Set Forests
| Autor: | Guttmann, Walter |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | Fundamenta Informaticae, Volume 192, Issue 1 (November 10, 2024) fi:10856 |
| Druh dokumentu: | Working Paper |
| Popis: | 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]. Comment: added explanations, simplified postconditions, restructured paper |
| Databáze: | arXiv |
| Externí odkaz: |
|