Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. An Axiomatization of Arrays for Kleene Algebra with Tests

An Axiomatization of Arrays for Kleene Algebra with Tests

File(s)
TR2006-2030.pdf (297.48 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5729
Collections
Computing and Information Science Technical Reports
Author
Aboul-Hosn, Kamal
Abstract

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.

Date Issued
2006-05-31
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2030
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance