• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Reasoning about Pointers in Refinement Calculus

Ralph-Johan Back, Xiaocong Fan, Viorel Preoteasa, Reasoning about Pointers in Refinement Calculus. In: Proceedings of the Tenth Asia-Pacific Software Engineering Conference (APSEC'03), 2003.

Abstract:

Pointers are an important programming concept. They are used
explicitely
or implicitly in many programming languages. In particular, the semantics
of object-oriented programming languages rely on pointers. We introduce
a semantics for pointer structures. Pointers are seen as indexes
and pointer fields are functions from these indexes to values. Using
this semantics we turn all pointer operations into simple assignments
and then we use refinement calculus techniques to construct a pointer-
manipulating
program that checks whether or not a single linked list has a loop.We
also introduce an induction principle on pointer structures in order
to reduce complexity of the proofs.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaFaPr03a,
  title = {Reasoning about Pointers in Refinement Calculus},
  booktitle = {Proceedings of the Tenth Asia-Pacific Software Engineering Conference (APSEC'03)},
  author = {Back, Ralph-Johan and Fan, Xiaocong and Preoteasa, Viorel},
  year = {2003},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication