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

翻译：本文研究如何使用关系代数,这些代数可用于高级规格和核实,以证明较低层次基于阵列的算法执行的正确性。 我们给出了在关联阵列上读写操作的简单关系代数语义。 阵列操作与支持同时编程的计算模型中的任务无缝结合。 因此, 关联代数可用于核查与关联阵列的程序。 我们使用逐级组合战略核查以阵列为基础的脱节森林执行的正确性, 并找到路径压缩、 路径分割和路径减半的操作。 所有结果都由伊莎贝尔/HOL正式证明。 本文是[1] 的扩展版本。