Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Reasoning about Pointers in Re...

Reasoning about Pointers in Refinement Calculus

Ralph-Johan Back, Xiaocong Fan, Viorel Preoteasa, Reasoning about Pointers in Refinement Calculus. TUCS Technical Reports 543, Turku Centre for Computer Science, 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:

@TECHREPORT{tBaX03a,
  title = {Reasoning about Pointers in Refinement Calculus},
  author = {Back, Ralph-Johan and Fan, Xiaocong and Preoteasa, Viorel},
  number = {543},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2003},
  ISBN = {952-12-1198-9},
}

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

Edit publication