The formal analysis of programs with arrays is a notoriously difficult problem due largely to aliasing considerations. In this paper we augment the rules of Kleene algebra with tests (
) with rules for the equational manipulation of arrays in the style of schematic
. These rules capture and make explicit the essence of
, where two array accesses can be to the same element. We prove the soundness of our rules, as well as illustrate their usefulness with several examples, including a complete proof of the correctness of heapsort.