Correctness of data representations involving heap data structures

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

Abstract

While the semantics of local variables in programming languages is by now well-understood, the semantics of pointer-addressed heap variables is still an outstanding issue. In particular, the commonly. assumed relational reasoning principles or data representations have not been validated in a semantic model of heap variables. In this paper, we define a parametricity semantics for a Pascal-like language with pointers and heap variables which gives such reasoning principles. It turns out that the correspondences between data representations cannot simply be relations between states, but more intricate correspondences that also need to keep track of visible locations whose pointers can be stored and leaked. (C) 2004 Elsevier B.V. All rights reserved.

Details

Original languageEnglish
Pages (from-to)129-160
Number of pages32
JournalScience of Computer Programming
Volume50
Issue number1-3
Publication statusPublished - 1 Jan 2004