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

翻译：本文研究如何利用关系代数（一种适用于高层规范与验证的工具）来证明低层基于数组的算法实现的正确性。我们为关联数组上的读写操作给出了简单的关系代数语义。这些数组操作能够无缝地集成到支持while程序的计算模型中的赋值操作里。由此，关系代数可用于验证包含关联数组的程序。我们验证了采用按秩合并策略的不相交集合森林的数组实现的正确性，并分别验证了带路径压缩、路径分裂和路径折半的查找操作。所有结果均在Isabelle/HOL中进行了形式化证明。本文是文献[1]的扩展版本。