Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
An Axiomatization of Arrays for Kleene Algebra with Tests
verfasst von : Kamal Aboul-Hosn
Erschienen in: Relations and Kleene Algebra in Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 (
KAT
) with rules for the equational manipulation of arrays in the style of schematic
KAT
. These rules capture and make explicit the essence of
subscript aliasing
, 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.