Relational Disjoint-Set Forests

Title:	Relational Disjoint-Set Forests
Author:	Walter Guttmann
Submission date:	2020-08-26
Abstract:	We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in the Hoare-logic library. Using relation algebras and Kleene algebras we verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression.
BibTeX:	@article{Relational_Disjoint_Set_Forests-AFP, author = {Walter Guttmann}, title = {Relational Disjoint-Set Forests}, journal = {Archive of Formal Proofs}, month = aug, year = 2020, note = {\url{https://isa-afp.org/entries/Relational_Disjoint_Set_Forests.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Stone_Kleene_Relation_Algebras
Used by:	Relational_Minimum_Spanning_Trees
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.